proposition: Lemma not_find_in_iff : forall m x, ~In x m <-> find x m = None.
proof: Proof. split; intros. - rewrite eq_option_alt. intro e. rewrite <- find_mapsto_iff. split; try discriminate. intro H'; elim H; exists e; auto. - intros (e,He); rewrite find_mapsto_iff,H in He; discriminate. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface