proposition: Lemma filter_not_in : ∀ elt k (m : M.t elt) P, ~ M.In (elt:=elt) k m → ~ M.In (elt:=elt) k (P.filter P m).
proof: Proof. intros. unfold P.filter. apply P.fold_rec_nodep; intros. unfold not; intros. apply F.empty_in_iff in H0. contradiction. destruct (P k0 e); auto. unfold not; intros. apply F.add_in_iff in H2; intuition. rewrite H3 in *; clear H3. apply H. apply in_mapsto_iff. exists e. assumption. Qed.
imports: Coq.Unicode.Utf8 Coq.FSets.FMapFacts