proposition: Lemma add_test_constraint_left_true_lb_cut : forall l1 u1 l2 u2 l u, add_test_constraint_left true (l1, u1) (l2, u2) = Some (l, u) -> l2 <> cp_max (comp_add l1 (cZ 1)) l2 -> l = comp_add l1 (cZ 1).
proof: Proof. intros [l1 | | ] [u1 | | ] [l2 | | ] [u2 | | ] l u; unfold add_test_constraint_left; 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 l u; clear H'); simpl; auto; (simpl; intro Hneq; destruct (Zmax_irreducible_inf (l1 + 1) l2) as [Hl1l2|Hl1l2]; try (rewrite Hl1l2 in Hneq;case Hneq; auto;fail); rewrite Hl1l2; auto; fail). Qed.
imports: ZArith List Lia