proposition: Lemma in_find m x `{!Ok m} : x ∈ m -> find x m <> None.
proof: Proof. intros (e,M). now rewrite (find_1 M). Qed.
imports: Coq(Bool Arith BinInt FunInd) Coq(Orders OrdersFacts OrdersLists) MMaps(Comparisons Interface OrdList)