proposition: Lemma diff_inter_cardinal : forall s s', cardinal (diff s s') + cardinal (inter s s') = cardinal s .
proof: Proof. intros; do 3 rewrite cardinal_fold. rewrite <- fold_plus. apply fold_diff_inter with (eqA:=@Logic.eq nat); auto with fset. Qed.
imports: FSetInterface PeanoNat DecidableTypeEx FSetFacts FSetDecide