proposition: Lemma filter_find (f : key -> elt -> bool) : Proper (K.eq==>eq==>eq) f -> forall m x, find x (filter f m) = option_bind (find x m) (fun e => if f x e then Some e else None).
proof: Proof. intros E m x. apply eq_option_alt. intros e. rewrite find_spec, filter_iff, <- find_spec; auto. split. - intros (-> & H'). simpl. now rewrite H'. - destruct (find x m); simpl; try easy. destruct f eqn:F; simpl; try easy. now intros [= ->]. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)