proposition: Lemma lbal_rb n l k e r : arbt n l -> rbt n r -> rbt (S n) (lbal l k e r).
proof: Proof. case lbal_match; intros; desarb; invrb; autom. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList Arith) Coq(Orders OrdersFacts OrdersLists) MMaps(Interface GenTree RBT)