proposition: Lemma mkEns_cardinal : forall s, cardinal _ (!!s) (M.cardinal s).
proof: Proof. intro s; pattern s; apply set_induction; clear s; intros. - intros; replace (!!s) with (Empty_set elt); auto with sets. + rewrite cardinal_1; auto with sets. + symmetry; apply Extensionality_Ensembles. apply Empty_Empty_set; auto. - replace (!!s') with (Add _ (!!s) x). + rewrite (cardinal_2 H0 H1); auto with sets. + symmetry; apply Extensionality_Ensembles. apply Add_Add; auto. Qed.
imports: Ensembles Finite_sets FSetInterface FSetProperties OrderedTypeEx DecidableTypeEx