proposition: Lemma cardinal_S m m' x e : ~ In x m -> Add x e m m' -> cardinal m' = S (cardinal m).
proof: Proof. intros. rewrite 2 cardinal_foldkeys. change S with ((fun _ => S) x). eapply foldkeys_Add with (eqA:=eq); eauto with *; congruence. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)