proposition: Lemma find_in_iff m x `{!Ok m} : find x m <> None <-> x ∈ m.
proof: Proof. split; auto using find_in, in_find. Qed.
imports: Coq(Bool Arith BinInt FunInd) Coq(Orders OrdersFacts OrdersLists) MMaps(Comparisons Interface OrdList)