proposition: Lemma elements_aux_cardinal : forall (m:t elt) acc, (length acc + cardinal m)%nat = length (elements_aux acc m).
proof: Proof. simple induction m; simpl; intuition. rewrite <- H; simpl. rewrite <- H0, Nat.add_succ_r, (Nat.add_comm (cardinal t)), Nat.add_assoc. reflexivity. Qed.
imports: FunInd FMapInterface FMapList ZArith Int