proposition: Lemma cardinal_foldkeys m : cardinal m = foldkeys (fun _ => S) m 0.
proof: Proof. apply cardinal_fold. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)