proposition: Lemma thinner_join : forall e1 e2 e3 e4, thinner e1 e2 -> thinner e3 e4 -> thinner (join e1 e3)(join e2 e4).
proof: Proof. intros [l1 u1] [l2 u2] [l3 u3][l4 u4]; unfold thinner; simpl; intros [H1 H2][H3 H4]; unfold join; split; simpl. destruct l1 as [l1 | | ]; destruct l2 as [l2 | | ]; simpl in H1, H2, H3, H4 |- *; try discriminate; auto; destruct l3 as [l3 | | ]; simpl in H1, H2, H3, H4 |- *; try discriminate; auto; destruct l4 as [l4 | | ]; simpl in H1, H2, H3, H4 |- *; try discriminate; auto. rewrite Z.min_assoc; rewrite <- (Z.min_assoc l1 l3 l2); rewrite (Z.min_comm l3 l2). injection H1; injection H3; clear H1 H3; intros H3 H1. rewrite Z.min_assoc; rewrite H1; rewrite <- Z.min_assoc; rewrite H3; auto. injection H1; clear H1; intros H1; rewrite Z.min_assoc; rewrite H1; auto. injection H3; clear H3; intros H3; rewrite Z.min_assoc; rewrite (Z.min_comm l3). rewrite <- Z.min_assoc; rewrite H3; auto. destruct u1 as [u1 | | ]; destruct u2 as [u2 | | ]; simpl in H1, H2, H3, H4 |- *; try discriminate; auto; destruct u3 as [u3 | | ]; simpl in H1, H2, H3, H4 |- *; try discriminate; auto; destruct u4 as [u4 | | ]; simpl in H1, H2, H3, H4 |- *; try discriminate; auto. injection H2; injection H4; clear H2 H4; intros H4 H2. rewrite Z.max_assoc; rewrite <- (Z.max_assoc u1); rewrite (Z.max_comm u3). rewrite Z.max_assoc; rewrite H2; rewrite <- Z.max_assoc; rewrite H4; auto. injection H2; clear H2; intros H2; rewrite Z.max_assoc; rewrite H2; auto. injection H4; clear H4; intros H4; rewrite Z.max_assoc; rewrite (Z.max_comm u3). rewrite <- Z.max_assoc; rewrite H4; auto. Qed.
imports: ZArith List Lia