proposition: Lemma rr_nrr_rb n t : rrt n t -> notredred t -> rbt n t.
proof: Proof. destruct 1 as [l x e r Hl Hr]. unfold rrcase; destmatch; now autom. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList Arith) Coq(Orders OrdersFacts OrdersLists) MMaps(Interface GenTree RBT)