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; simpl in *; lia_max. Qed.
imports: Coq(ZArith Int Lia PeanoNat FunInd Orders) MMaps(GenTree AVL)