mathlib

3ff3f2d6 - feat(set_theory/cardinal/finite): prove lemmas to handle part_enat.card (#19198)

feat(set_theory/cardinal/finite): prove lemmas to handle part_enat.card (#19198) Prove some lemmas that allow to handle part_enat.card of finite cardinals, analogous to those about nat.card Co-authored-by: Antoine Chambert-Loir <antoine.chambert-loir@math.univ-paris-diderot.fr>