proposition: Lemma append_avl_1 : forall s1 s2 `{!Avl s1, !Avl s2}, -(2) <= height s1 - height s2 <= 2 -> Avl (append s1 s2) /\ 0<= height (append s1 s2) - max (height s1) (height s2) <=1.
proof: Proof. intros s1 s2; functional induction (append s1 s2); intros; try (factornode s1). - simpl; split; auto; avl_nns; lia_max. - simpl; split; auto; avl_nns; simpl in *; lia_max. - generalize (@remove_min_avl_1 l2 x2 d2 r2 _ _). mysubst. destruct 1; simpl in *. split. * apply bal_avl; trivial. simpl; lia_max. * lia_bal. Qed.
imports: Coq(ZArith Int Lia PeanoNat FunInd Orders) MMaps(GenTree AVL)