proposition: Lemma cardinal_notin_add m x e : ~In x m -> cardinal (add x e m) = S (cardinal m).
proof: Proof. intros NI. eapply cardinal_S; eauto using Add_add. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)