proposition: Lemma Equal_cardinal : forall s s', s[=]s' -> cardinal s = cardinal s'.
proof: Proof. symmetry. remember (cardinal s) as n; symmetry in Heqn; revert s s' Heqn H. induction n; intros. - apply cardinal_1; rewrite <- H; auto with fset. - destruct (cardinal_inv_2 Heqn) as (x,H2). revert Heqn. rewrite (cardinal_2 (s:=remove x s) (s':=s) (x:=x)); auto with set. rewrite (cardinal_2 (s:=remove x s') (s':=s') (x:=x)); eauto with set. Qed.
imports: FSetInterface PeanoNat DecidableTypeEx FSetFacts FSetDecide