proposition: Lemma lbalS_arb n l x e r : arbt n l -> rbt (S n) r -> arbt (S n) (lbalS l x e r).
proof: Proof. case lbalS_match. - destruct 1; invrb; autom. - clear l. intros l Hl Hl' Hr. destruct r as [|[|] rl rx rv rr]; invrb. * destruct rl as [|[|] rll rlx rlv rlr]; invrb. right; auto using rbal'_rb, makeRed_rr with map. * left; apply rbal'_rb; autom. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList Arith) Coq(Orders OrdersFacts OrdersLists) MMaps(Interface GenTree RBT)