proposition: Lemma arb_nr_rb n t : arbt n t -> notred t -> rbt n t.
proof: Proof. destruct 1; destruct t; descolor; invrb; autom. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList Arith) Coq(Orders OrdersFacts OrdersLists) MMaps(Interface GenTree RBT)