proposition: Lemma rbalS_rb n l x r : rbt (S n) l -> notred l -> arbt n r -> rbt (S n) (rbalS l x r).
proof: Proof. intros Hl Hl' Hr. destruct l as [|[|] ll lx lr]; invrb. clear Hl'. revert Hr. case rbalS_match. - destruct 1; invrb; auto. - intros. apply lbal_rb; auto. Qed.
imports: Bool List BinPos Pnat Setoid SetoidList PeanoNat