proposition: Lemma makeBlack_rb n t : arbt n t -> Rbt (makeBlack t).
proof: Proof. destruct t as [|[|] l x e r]. - exists 0; simpl; autom. - destruct 1; invrb; exists (S n); simpl; autom. - exists n; autom. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList Arith) Coq(Orders OrdersFacts OrdersLists) MMaps(Interface GenTree RBT)