proposition: Lemma merge_avl_1 : forall m1 m2, avl m1 -> avl m2 -> -(2) <= height m1 - height m2 <= 2 -> avl (merge m1 m2) /\ 0<= height (merge m1 m2) - max (height m1) (height m2) <=1.
proof: Proof. intros m1 m2; functional induction (merge m1 m2); intros; try factornode _x _x0 _x1 _x2 _x3 as m1. - simpl; split; auto; avl_nns; omega_max. - simpl; split; auto; avl_nns; omega_max. - generalize (remove_min_avl_1 H0). rewrite e1; destruct 1. split. + apply bal_avl; auto. omega_max. + omega_bal. Qed.
imports: FunInd Recdef FMapInterface FMapList ZArith Int FMapAVL Lia