fact: Definition cardinal U (A : Ensemble U) (n : nat) : Prop := exists ls, EnsembleListEquivalence A ls /\ Datatypes.length ls = n.
imports: Coq.Lists.List Coq.Sets.Ensembles Fiat.Common Fiat.Common.List.PermutationFacts Fiat.Common.Ensembles.EnsembleListEquivalence