proposition: Lemma del_in m x y `{!Ok m} : y ∈ (del x m) <-> y ∈ m /\ ~ y==x.
proof: Proof. induct m; destmatch; autorew; try rewrite IHl; try rewrite IHr; try clear IHl IHr; treeorder. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)