proposition: Lemma is_empty_2 : is_empty m = true -> Empty m.
proof: Proof. induction m; simpl; auto. - rewrite Empty_alt. intros _; exact gempty. - rewrite Empty_Node. destruct o. + intros; discriminate. + intro H; destruct (andb_prop _ _ H); intuition. Qed.
imports: Bool OrderedType ZArith OrderedType OrderedTypeEx FMapInterface