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; auto. Qed.
imports: FunInd Recdef FMapInterface FMapList ZArith Int FMapAVL Lia