proposition: Lemma rbalS_rb n l x e r : rbt (S n) l -> notred l -> arbt n r -> rbt (S n) (rbalS l x e r).
proof: Proof. intros Hl Hl' Hr. destruct l as [|[|] ll lx lv lr]; invrb. clear Hl'. revert Hr. case rbalS_match. - destruct 1; invrb; autom. - intros. apply lbal_rb; autom. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList Arith) Coq(Orders OrdersFacts OrdersLists) MMaps(Interface GenTree RBT)