proposition: Lemma join_avl_1 l x e r : forall `{!Avl l, !Avl r}, Avl (join l x e r) /\ 0<= height (join l x e r) - max (height l) (height r) <= 1.
proof: Proof. join_tac l x e r; clearf. - simpl. destruct (@add_avl_1 r x e); auto. split; trivial. avl_nns; lia_max. - remtree (Node lh ll lx ld lr) l. split; autok. destruct (@add_avl_1 l x e); auto. simpl. avl_nns; lia_max. - remtree (Node rh rl rx rd rr) r. inv_avl. destruct (Hlr x e r); trivial; clear Hrl Hlr. set (j := join lr x e r) in *; clearbody j. simpl. assert (-(3) <= height ll - height j <= 3) by lia_max. split. * apply bal_avl; trivial. * lia_bal. - remtree (Node lh ll lx ld lr) l. inv_avl. destruct Hrl; trivial; clear Hlr. set (j := join l x e rl) in *; clearbody j. simpl. assert (-(3) <= height j - height rr <= 3) by lia_max. split. * apply bal_avl; trivial. * lia_bal. - clear Hrl Hlr. remtree (Node lh ll lx ld lr) l. remtree (Node rh rl rx rd rr) r. assert (-(2) <= height l - height r <= 2) by lia_max. split. * apply create_avl; trivial. * rewrite create_height; trivial; lia_max. Qed.
imports: Coq(ZArith Int Lia PeanoNat FunInd Orders) MMaps(GenTree AVL)