proposition: Lemma rbalS_arb n l x e r : rbt (S n) l -> arbt n r -> arbt (S n) (rbalS l x e r).
proof: Proof. case rbalS_match. - destruct 2; invrb; autom. - clear r. intros r Hr Hr' Hl. destruct l as [|[|] ll lx lv lr]; invrb. * destruct lr as [|[|] lrl lrx lrv lrr]; invrb. right; auto using lbal_rb, makeRed_rr with map. * left; apply lbal_rb; autom. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList Arith) Coq(Orders OrdersFacts OrdersLists) MMaps(Interface GenTree RBT)