proposition: Lemma filter_add_false : ∀ elt k (e : elt) m m' P, Proper (E.eq ==> eq ==> eq) P → ~ M.In (elt:=elt) k m → M.Equal (P.filter P (M.add k e m)) m' → P k e = false → M.Equal (P.filter P m) m'.
proof: Proof. intros. rewrite <- H1; clear H1. apply F.Equal_mapsto_iff; split; intros. simplify_maps. simplify_maps; intuition. simplify_maps. right; intuition. rewrite <- H1 in H3. contradiction H0. apply in_mapsto_iff. exists e0; assumption. simplify_maps. simplify_maps. rewrite H1 in H2. congruence. simplify_maps. Qed.
imports: Coq.Unicode.Utf8 Coq.FSets.FMapFacts