proposition: Lemma cardinal_fold m : cardinal m = fold (fun _ _ => S) m 0.
proof: Proof. rewrite cardinal_1, fold_1. symmetry; apply fold_left_length; auto. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)