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