proposition: Lemma makeBlack_rb n t : arbt n t -> Rbt (makeBlack t).
proof: Proof. destruct t as [|[|] l x r]. - exists 0; auto. - destruct 1; invrb; exists (S n); simpl; auto. - exists n; auto. Qed.
imports: Bool List BinPos Pnat Setoid SetoidList PeanoNat