proposition: Lemma bal_avl : forall l x e r `{!Avl l, !Avl r}, -(3) <= height l - height r <= 3 -> Avl (bal l x e r).
proof: Proof. intros l x e r; functional induction (bal l x e r); intros; clearf; inv_avl; simpl in *; try (when assert_false; avl_nns); repeat apply create_avl; simpl in *; auto; lia_max. Qed.
imports: Coq(ZArith Int Lia PeanoNat FunInd Orders) MMaps(GenTree AVL)