proposition: Theorem union_inter_cardinal : forall s s', cardinal (union s s') + cardinal (inter s s') = cardinal s + cardinal s' .
proof: Proof. intros. do 4 rewrite cardinal_fold. do 2 rewrite <- fold_plus. apply fold_union_inter with (eqA:=@Logic.eq nat); auto with *. congruence. Qed.
imports: MSetInterface PeanoNat DecidableTypeEx OrdersLists MSetFacts MSetDecide