proposition: Lemma Partition_cardinal m m1 m2 : Partition m m1 m2 -> cardinal m = cardinal m1 + cardinal m2.
proof: Proof. intros. rewrite (cardinal_fold m), (cardinal_fold m1). set (f:=fun (_:key)(_:elt)=>S). setoid_replace (fold f m 0) with (fold f m1 (fold f m2 0)). rewrite <- cardinal_fold. apply fold_rel with (R:=fun u v => u = v + cardinal m2); simpl; auto. apply Partition_fold with (eqA:=eq); compute; auto with map. congruence. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)