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