proposition: Lemma makeRed_rr t n : rbt (S n) t -> notred t -> rrt n (makeRed t).
proof: Proof. destruct t as [|[|] l x e r]; invrb; simpl; autom. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList Arith) Coq(Orders OrdersFacts OrdersLists) MMaps(Interface GenTree RBT)