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 *; match goal with |- avl (assert_false _ _ _ _) => avl_nns | _ => repeat apply create_avl; simpl in *; auto end; omega_max. Qed.
imports: FunInd Recdef FMapInterface FMapList ZArith Int FMapAVL Lia