proposition: Lemma filter_Empty : ∀ elt (m : M.t elt) P, M.Empty (elt:=elt) m → M.Empty (elt:=elt) (P.filter P m).
proof: Proof. intros. unfold P.filter. revert H. apply P.fold_rec; intros. apply M.empty_1. specialize (H1 k). unfold P.Add in H1. rewrite F.elements_o in H1. apply P.elements_Empty in H3. rewrite H3 in H1; simpl in H1. rewrite F.add_eq_o in H1; [| apply E.eq_refl]. discriminate. Qed.
imports: Coq.Unicode.Utf8 Coq.FSets.FMapFacts