proposition: Lemma add_avl_1 : forall m x e, avl m -> avl (add x e m) /\ 0 <= height (add x e m) - height m <= 1.
proof: Proof. intros m x e; functional induction (add x e m); intros; inv avl; simpl in *. - intuition; try constructor; simpl; auto; try omega_max. - destruct IHt; auto. split. + apply bal_avl; auto; omega_max. + omega_bal. - intuition; omega_max. - destruct IHt; auto. split. + apply bal_avl; auto; omega_max. + omega_bal. Qed.
imports: FunInd Recdef FMapInterface FMapList ZArith Int FMapAVL Lia