proposition: Lemma rbalS_arb n l x r : rbt (S n) l -> arbt n r -> arbt (S n) (rbalS l x r).
proof: Proof. case rbalS_match. - destruct 2; invrb; auto. - clear r. intros r Hr Hr' Hl. destruct l as [|[|] ll lx lr]; invrb. * destruct lr as [|[|] lrl lrx lrr]; invrb. right; auto using lbal_rb, makeRed_rr. * left; apply lbal_rb; auto. Qed.
imports: Bool List BinPos Pnat Setoid SetoidList PeanoNat