proposition: Lemma add_test_constraint_left_false_monotonic : forall v1 v2 v1' v2' v v', add_test_constraint_left false v1 v2 = Some v -> add_test_constraint_left 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_left_false_lb with (1:=H). rewrite add_test_constraint_left_false_lb with (1:=H'). destruct (ext_eq u2 (cp_min u1 u2)) as [Hl1l2 | Hl1l2]. rewrite add_test_constraint_left_false_lb_no_cut with (1:=H); auto. destruct (ext_eq u2' (cp_min u1' u2')). rewrite add_test_constraint_left_false_lb_no_cut with (1:=H'); auto. rewrite add_test_constraint_left_false_lb_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. apply cp_min_r_cp_max_l; auto. rewrite add_test_constraint_left_false_lb_cut with (1:=H); auto. destruct (ext_eq u2' (cp_min u1' u2')). rewrite add_test_constraint_left_false_lb_no_cut with (1:=H'); auto. intros [H1 H2][H3 H4]; split; auto. rewrite cp_max_comm; apply cp_max_trans with u2. rewrite cp_max_comm; auto. apply cp_min_r_cp_max_l. rewrite cp_min_comm. case (cp_min_irreducible u1 u2); auto; intros; case Hl1l2; auto. rewrite add_test_constraint_left_false_lb_cut with (1:=H'); auto. intros [H1 H2][H3 H4];split; auto. Qed.
imports: ZArith List Lia