proposition: Lemma add_test_constraint_right_true_none : forall v1 v2, add_test_constraint_right true v1 v2 = None -> forall x1 x2, to_p v1 x1 -> to_p v2 x2 -> ~x1 < x2.
proof: Proof. intros [b1 u1] [b2 u2]; unfold add_test_constraint_right. case (ext_eq b1 (cp_max b1 u2)); intros Heq. intros _; destruct b1 as [b1 | | ]; destruct u2 as [u2 | | ]; try (assert (H' : u2 <= b1) by(injection Heq; intros h; rewrite h; apply Z.le_max_r)); destruct u1 as [u1 | | ]; simpl in Heq; try discriminate heq; simpl; intros e1 e2 g; simpl; try(intuition;fail); try discriminate; destruct b2 as [b2 | | ]; simpl; try(intuition;fail). intros; discriminate. Qed.
imports: ZArith List Lia