proposition: Lemma create_avl : forall l x e r `{!Avl l, !Avl r}, -(2) <= height l - height r <= 2 -> Avl (create l x e r).
proof: Proof. unfold create; autom. Qed.
imports: Coq(ZArith Int Lia PeanoNat FunInd Orders) MMaps(GenTree AVL)