proposition: Lemma find_in m x : find x m <> None -> x ∈ m.
proof: Proof. destruct (find x m) eqn:F; intros H. - exists e. now apply find_2. - now elim H. Qed.
imports: Coq(Bool Arith BinInt FunInd) Coq(Orders OrdersFacts OrdersLists) MMaps(Comparisons Interface OrdList)