proposition: Lemma add_test_constraint_left_false_sound : forall v1 v2 v x1 x2, add_test_constraint_left false v1 v2 = Some v -> to_p v1 x1 -> to_p v2 x2 -> ~ x1 < x2 -> to_p v x2.
proof: Proof. intros [b1 u1][b2 u2] v x1 x2; unfold add_test_constraint_left. case (ext_eq b2 (cp_max u1 b2)); intros Heq. case (ext_eq u1 (cp_max u1 b2)); intros Heq'; try (intros; discriminate); intros H'; injection H'; intro ; subst v; clear H'; destruct b1 as [b1 | | ]; destruct u1 as [u1 | | ]; simpl; try (simpl;intuition;fail); destruct b2 as [b2 | | ]; destruct u2 as [u2 | | ]; simpl; try (simpl;intuition;fail); try (intros;discriminate); try (case (Zmin_irreducible u1 u2); lia). intros H'; injection H'; intro; subst v; clear H'. destruct b1 as [b1 | | ]; destruct u1 as [u1 | | ]; simpl; try (simpl;intuition;fail); destruct b2 as [b2 | | ]; try (assert (H': b2 <> u1) by (intro; elim Heq; subst b2; rewrite cp_max_refl; auto)); destruct u2 as [u2 | | ]; try case (Zmin_irreducible_inf u1 u2); simpl; try (simpl;intuition;fail); try (intros;discriminate). Qed.
imports: ZArith List Lia