proposition: Lemma add_test_constraint_right_true_monotonic : forall v1 v2 v1' v2' v v', add_test_constraint_right true v1 v2 = Some v -> add_test_constraint_right 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_right_true_lb with (1:=H). rewrite add_test_constraint_right_true_lb with (1:=H'). destruct (ext_eq u1 (cp_min u1 (comp_add u2 (cZ (-1))))). rewrite add_test_constraint_right_true_ub_no_cut with (1:=H); auto. destruct (ext_eq u1' (cp_min u1' (comp_add u2' (cZ (-1))))). rewrite add_test_constraint_right_true_ub_no_cut with (1:=H'); auto. rewrite add_test_constraint_right_true_ub_cut with (1:=H'); auto. intros [H1 H2][H3 H4]; split; auto. rewrite cp_max_comm; apply cp_max_trans with (comp_add u2 (cZ (-1))). destruct u2 as [u2 | | ]; destruct u2' as [u2' | | ]; simpl in *; try discriminate; auto. assert (u2 <= u2') by (injection H4; intros a; rewrite <- a; apply Z.le_max_l). rewrite Zle_to_Zmax; auto; try lia. apply cp_min_r_cp_max_l; rewrite cp_min_comm; auto. rewrite add_test_constraint_right_true_ub_cut with (1:=H); auto. destruct (ext_eq u1' (cp_min u1' (comp_add u2' (cZ (-1))))). rewrite add_test_constraint_right_true_ub_no_cut with (1:=H'); auto. intros [H1 H2][H3 H4]; split; auto. rewrite cp_max_comm; apply cp_max_trans with u1. rewrite cp_max_comm; auto. rewrite cp_max_comm; apply not_cp_min_cp_max; rewrite cp_min_comm; auto. rewrite add_test_constraint_right_true_ub_cut with (1:=H'); auto. intros [H1 H2][H3 H4]; split; auto. rewrite cp_max_comm; rewrite cp_max_plus; auto. rewrite cp_max_comm; auto. Qed.
imports: ZArith List Lia