proposition: Lemma remove_spec1 m x `{!Ok m} : find x (remove x m) = None.
proof: Proof. unfold remove. rewrite makeBlack_find. now apply del_spec1. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)