proposition: Lemma avl_node : forall x e l r, avl l -> avl r -> -(2) <= height l - height r <= 2 -> avl (Node l x e r (max (height l) (height r) + 1)).
proof: Proof. intros; auto. Qed.
imports: FunInd Recdef FMapInterface FMapList ZArith Int FMapAVL Lia