proposition: Lemma mem_spec m x `{!Ok m} : mem x m = true <-> x ∈ m.
proof: Proof. induction m; simpl. - now rewrite in_leaf. - invok. rewrite in_node. case K.compare_spec; intuition; order. Qed.
imports: Coq(Bool Arith BinInt FunInd) Coq(Orders OrdersFacts OrdersLists) MMaps(Comparisons Interface OrdList)