proposition: Lemma cardinal_In_Add m m' x e : In x m -> Add x e m m' -> cardinal m' = cardinal m.
proof: Proof. intros IN AD. apply Eqdom_cardinal. apply Equal_Eqdom in AD. rewrite AD. now rewrite <- Eqdom_in_add. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)