proposition: Lemma bal_height_1 : forall l x e r `{!Avl l, !Avl r}, -(3) <= height l - height r <= 3 -> 0 <= 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 *; lia_max. Qed.
imports: Coq(ZArith Int Lia PeanoNat FunInd Orders) MMaps(GenTree AVL)