proposition: Lemma cardinal_1 : forall (m: t A), cardinal m = length (elements m).
proof: Proof. unfold elements. intros m; set (p:=1); clearbody p; revert m p. induction m; simpl; auto; intros. rewrite (IHm1 (append p 2)), (IHm2 (append p 3)). destruct o; rewrite app_length; simpl; auto. Qed.
imports: Bool OrderedType ZArith OrderedType OrderedTypeEx FMapInterface