proposition: Lemma add_test_constraint_right_true_sound : forall v1 v2 v x1 x2, add_test_constraint_right true v1 v2 = Some v -> to_p v1 x1 -> to_p v2 x2 -> x1 < x2 -> to_p v x1.
proof: Proof. intros [b1 u1][b2 u2] v x1 x2; unfold add_test_constraint_right. case (ext_eq b1 (cp_max b1 u2)); intros Heq; try (intros; discriminate). intros Hres; injection Hres; intro; subst v. intros H1 H2 H'; destruct (to_p_cp_max_min _ _ _ H1) as [H3 H4]. destruct (to_p_cp_max_min _ _ _ H2) as [H5 H6]. apply cp_max_min_to_p; auto. destruct u1 as [u1 | | ]; try (simpl; intuition;fail); destruct u2 as [u2 | | ]; try (simpl; intuition; fail); simpl; try (intros; discriminate). assert (x1 <= u1) by (simpl in H4; injection H4; intros H7; rewrite <- H7; apply Z.le_min_r). assert (x2 <= u2) by (simpl in H6; injection H6; intros H7; rewrite <- H7; apply Z.le_min_r). destruct (Zle_or_lt u1 (u2+ -1)). rewrite (Zle_to_Zmin u1); try lia. rewrite Zle_to_Zmin; auto. rewrite (Z.min_comm u1); rewrite (Zle_to_Zmin (u2+ -1)); try lia. rewrite Zle_to_Zmin; auto; lia. assert (x2 <= u2) by (simpl in H6; injection H6; intros H7; rewrite <- H7; apply Z.le_min_r). rewrite Zle_to_Zmin; auto; lia. Qed.
imports: ZArith List Lia