proposition: Lemma cardinal_fold : forall m : t elt, cardinal m = fold (fun _ _ => S) m 0.
proof: Proof. intros; rewrite cardinal_1, fold_1. symmetry; apply fold_left_length; auto. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface