proposition: Lemma del_spec1 m x `{!Ok m} : find x (del x m) = None.
proof: Proof. apply not_find_iff; ok. rewrite del_in; treeorder. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)