proposition: Lemma lbalS_arb n l x r : arbt n l -> rbt (S n) r -> arbt (S n) (lbalS l x r).
proof: Proof. case lbalS_match. - destruct 1; invrb; auto. - clear l. intros l Hl Hl' Hr. destruct r as [|[|] rl rx rr]; invrb. * destruct rl as [|[|] rll rlx rlr]; invrb. right; auto using rbal'_rb, makeRed_rr. * left; apply rbal'_rb; auto. Qed.
imports: Bool List BinPos Pnat Setoid SetoidList PeanoNat