proposition: Lemma lbalS_rb n l x e r : arbt n l -> rbt (S n) r -> notred r -> rbt (S n) (lbalS l x e r).
proof: Proof. intros Hl Hr Hr'. destruct r as [|[|] rl rx rv rr]; invrb. clear Hr'. revert Hl. case lbalS_match. - destruct 1; invrb; autom. - intros. apply rbal'_rb; autom. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList Arith) Coq(Orders OrdersFacts OrdersLists) MMaps(Interface GenTree RBT)