proposition: Lemma add_test_constraint_left_true_monotonic : forall v1 v2 v1' v2' v v', add_test_constraint_left true v1 v2 = Some v -> add_test_constraint_left true v1' v2' = Some v' -> thinner v1 v1' -> thinner v2 v2' -> thinner v v'.
proof: Proof. intros [l1 u1][l2 u2][l1' u1'][l2' u2'][l u][l' u'] H H'. rewrite add_test_constraint_left_true_ub with (1:=H). rewrite add_test_constraint_left_true_ub with (1:=H'). destruct (ext_eq l2 (cp_max (comp_add l1 (cZ 1)) l2)) as [Hl2l1 | Hl2l1]. rewrite add_test_constraint_left_true_lb_no_cut with (1:=H); auto. destruct (ext_eq l2' (cp_max (comp_add l1' (cZ 1)) l2')). rewrite add_test_constraint_left_true_lb_no_cut with (1:=H'); auto. rewrite add_test_constraint_left_true_lb_cut with (1:=H'); auto. intros [H1 H2][H3 H4]; split; auto. rewrite cp_min_comm; apply cp_min_trans with (comp_add l1 (cZ 1)). destruct l1 as [l1 | | ]; destruct l1' as [l1' | | ]; simpl in *; try discriminate; auto. assert (l1' <= l1) by (injection H1; intros a; rewrite <- a; apply Z.le_min_l). rewrite Zle_to_Zmin; auto; try lia. apply cp_max_r_cp_min_l; auto. rewrite add_test_constraint_left_true_lb_cut with (1:=H); auto. destruct (ext_eq l2' (cp_max (comp_add l1' (cZ 1)) l2')). rewrite add_test_constraint_left_true_lb_no_cut with (1:=H'); auto. intros [H1 H2][H3 H4]; split; auto. rewrite cp_min_comm; apply cp_min_trans with l2. rewrite cp_min_comm; auto. apply cp_max_r_cp_min_l; rewrite cp_max_comm; case (cp_max_irreducible (comp_add l1 (cZ 1)) l2); try (intros; case Hl2l1; auto; fail); auto. rewrite add_test_constraint_left_true_lb_cut with (1:=H'); auto. intros [H1 H2][H3 H4]; split; auto. rewrite cp_min_comm; rewrite cp_min_plus; auto. rewrite cp_min_comm; auto. Qed.
imports: ZArith List Lia