proposition: Lemma cardinal_fold : forall s, cardinal s = fold (fun _ => S) s 0.
proof: Proof. intros; rewrite cardinal_1; rewrite M.fold_1. symmetry; apply fold_left_length; auto. Qed.
imports: FSetInterface PeanoNat DecidableTypeEx FSetFacts FSetDecide