proposition: Lemma add_test_constraint_right_monotonic_none : forall neg v1 v2 v1' v2' v, add_test_constraint_right neg v1 v2 = Some v -> thinner v1 v1' -> thinner v2 v2' -> ~add_test_constraint_right neg v1' v2' = None.
proof: Proof. unfold add_test_constraint_right; intros [|] [l1 u1][l2 u2][l1' u1'][l2' u2'] [l u] Hadd [H1 H2][H3 H4]. destruct (ext_eq l1' (cp_max l1' u2')). destruct (ext_eq l1 (cp_max l1 u2)) as [A | B]; try discriminate. destruct B; symmetry. apply cp_max_trans with l1'. apply cp_min_r_cp_max_l; auto. apply cp_max_trans with u2'; auto. rewrite cp_max_comm; auto. discriminate. destruct (ext_eq l2' (cp_max u1' l2')) as [C | D]; try discriminate. destruct (ext_eq u1' (cp_max u1' l2')) as [A | B]; try discriminate. destruct B; symmetry. destruct (ext_eq l2 (cp_max u1 l2)) as [A | B]; try discriminate. destruct (ext_eq u1 (cp_max u1 l2)); try discriminate. apply cp_max_trans with u1. rewrite cp_max_comm; auto. apply cp_max_trans with l2; auto. apply cp_min_r_cp_max_l; auto. apply cp_max_trans with u1. rewrite cp_max_comm; auto. apply cp_max_trans with l2. case (cp_max_irreducible u1 l2); auto; intros; case B; auto. apply cp_min_r_cp_max_l; auto. Qed.
imports: ZArith List Lia