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