proposition: Lemma diff_in_iff : forall m m' k, In k (diff m m') <-> In k m /\ ~In k m'.
proof: Proof. intros m m' k. split. - intros (e,H); rewrite diff_mapsto_iff in H. destruct H; split; auto. exists e; auto. - intros ((e,H),H'); exists e; rewrite diff_mapsto_iff; auto. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface