proposition: Lemma add_test_constraint_right_false_none : forall v1 v2, add_test_constraint_right false 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 b2 (cp_max u1 b2)); intros Heq; case (ext_eq u1 (cp_max u1 b2)); intros Heq'; try (intros; discriminate). intros _; destruct b2 as [b2 | | ]; destruct u1 as [u1 | | ]; try (assert (H' : u1 <= b2) by (injection Heq; intros h; rewrite h; apply Z.le_max_l)); try (assert (H'' : ~u1 = b2) by (intros h; subst u1; elim Heq'; rewrite cp_max_refl; auto)); simpl; try (intuition; fail); destruct u2 as [u2 | | ]; try discriminate Heq; simpl; intros e1 e2 g; simpl; try(intuition;fail); try discriminate; destruct b1 as [b1 | | ]; simpl; try(intuition;fail). Qed.
imports: ZArith List Lia