proposition: Lemma Proper_Oeq_negb : ∀ B f, Proper (E.eq ==> eq ==> eq) f -> Proper (E.eq ==> eq ==> eq) (fun (k : M.key) (e : B) => negb (f k e)).
proof: Proof. intros ?????????; f_equal; subst; rewrite H0; reflexivity. Qed.
imports: Coq.Unicode.Utf8 Coq.FSets.FMapFacts