proposition: Lemma add_test_constraint_right_false_monotonic : forall v1 v2 v1' v2' v v', add_test_constraint_right false v1 v2 = Some v -> add_test_constraint_right false 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_false_ub with (1:=H). rewrite add_test_constraint_right_false_ub with (1:=H'). destruct (ext_eq l1 (cp_max l1 l2)) as [Hl1l2 | Hl1l2]. rewrite add_test_constraint_right_false_lb_no_cut with (1:=H); auto. destruct (ext_eq l1' (cp_max l1' l2')). rewrite add_test_constraint_right_false_lb_no_cut with (1:=H'); auto. rewrite add_test_constraint_right_false_lb_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; auto. rewrite add_test_constraint_right_false_lb_cut with (1:=H); auto. destruct (ext_eq l1' (cp_max l1' l2')). rewrite add_test_constraint_right_false_lb_no_cut with (1:=H'); auto. intros [H1 H2][H3 H4]; split; auto. rewrite cp_min_comm; apply cp_min_trans with l1. rewrite cp_min_comm; auto. apply cp_max_r_cp_min_l. case (cp_max_irreducible l1 l2); auto; intros; case Hl1l2; auto. rewrite add_test_constraint_right_false_lb_cut with (1:=H'); auto. intros [H1 H2][H3 H4];split; auto. Qed.
imports: ZArith List Lia