proposition: Lemma add_test_constraint_right_true_ub_cut : forall l1 u1 l2 u2 l u, add_test_constraint_right true (l1, u1) (l2, u2) = Some (l, u) -> u1 <> cp_min u1 (comp_add u2 (cZ (-1))) -> u = comp_add u2 (cZ (-1)).
proof: Proof. intros [l1 | | ] [u1 | | ] [l2 | | ] [u2 | | ] l u; unfold add_test_constraint_right; try (match goal with |- context[ext_eq ?a ?b] => case (ext_eq a b); intros Heq end); try (simpl; intros; intuition; discriminate); try (intros H'; injection H'; do 2 intro; subst u; clear H'); try (simpl; intro Hneq; destruct (Zmin_irreducible u1 (u2+ -1)) as [H|H]; try (rewrite H in Hneq;case Hneq; auto;fail); rewrite H; auto; fail); simpl; auto. Qed.
imports: ZArith List Lia