proposition: Lemma find_1 m x e `{!Ok m} : m@x ↦ e -> find x m = Some e.
proof: Proof. induction m; simpl; invok. - intuition_m. - rewrite node_mapsto. case K.compare_spec; intuition_m; subst; auto; order. Qed.
imports: Coq(Bool Arith BinInt FunInd) Coq(Orders OrdersFacts OrdersLists) MMaps(Comparisons Interface OrdList)