proposition: Lemma lbalS_rb n l x r : arbt n l -> rbt (S n) r -> notred r -> rbt (S n) (lbalS l x r).
proof: Proof. intros Hl Hr Hr'. destruct r as [|[|] rl rx rr]; invrb. clear Hr'. revert Hl. case lbalS_match. - destruct 1; invrb; auto. - intros. apply rbal'_rb; auto. Qed.
imports: Bool List BinPos Pnat Setoid SetoidList PeanoNat