proposition: Lemma add_test_constraint_left_true_sound : forall v1 v2 v x1 x2, add_test_constraint_left true 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 u2 (cp_min b1 u2)); intros Heq; try (intros; discriminate). intros Hres; injection Hres; intro; subst v. destruct b1 as [b1 | | ]; try (simpl; intuition;fail); destruct u1 as [u1 | | ]; try (simpl; intuition;fail); destruct b2 as [b2 | | ]; try (simpl; intuition;fail); destruct u2 as [u2 | | ]; try (simpl; intuition; fail); simpl; try (assert (b1 <> u2) by (intros h;subst u2; elim Heq; rewrite cp_min_refl; auto)); try (case (Zmax_irreducible_inf (b1+1) b2);(intros; lia)); try (intros; lia). Qed.
imports: ZArith List Lia