proposition: Lemma elements_in_iff : forall m x, In x m <-> exists e, InA (@eq_key_elt _) (x,e) (elements m).
proof: Proof. unfold In; split; intros (e,H); exists e; [apply elements_1 | apply elements_2]; auto. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface