proposition: Lemma avl_node : forall x e l r `{!Avl l, !Avl r}, -(2) <= height l - height r <= 2 -> Avl (Node (max (height l) (height r) + 1) l x e r).
proof: Proof. autok. Qed.
imports: Coq(ZArith Int Lia PeanoNat FunInd Orders) MMaps(GenTree AVL)