fact: Axiom 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.
imports: syntax little denot Bool List String ZArith axiom