proposition: Lemma find_2 m x e : find x m = Some e -> m@x ↦ e.
proof: Proof. induction m; simpl; try easy. case K.compare_spec; [ intros -> [= ->] | .. ]; intuition_m. Qed.
imports: Coq(Bool Arith BinInt FunInd) Coq(Orders OrdersFacts OrdersLists) MMaps(Comparisons Interface OrdList)