proposition: Lemma bal_height_2 : forall l x e r, avl l -> avl r -> -(2) <= height l - height r <= 2 -> height (bal l x e r) == max (height l) (height r) +1.
proof: Proof. intros l x e r; functional induction (bal l x e r); intros; clearf; inv avl; avl_nns; simpl in *; omega_max. Qed.
imports: FunInd Recdef FMapInterface FMapList ZArith Int FMapAVL Lia