diff options
Diffstat (limited to 'test-suite/micromega/non_lin_ci.v')
| -rw-r--r-- | test-suite/micromega/non_lin_ci.v | 24 |
1 files changed, 12 insertions, 12 deletions
diff --git a/test-suite/micromega/non_lin_ci.v b/test-suite/micromega/non_lin_ci.v index ec39209230..2a66cc9a5a 100644 --- a/test-suite/micromega/non_lin_ci.v +++ b/test-suite/micromega/non_lin_ci.v @@ -43,18 +43,18 @@ Proof. Qed. Goal - forall (__x1 __x2 __x3 __x4 __x5 __x6 __x7 __x8 __x9 __x10 __x11 __x12 __x13 - __x14 __x15 __x16 : Z) - (H6 : __x8 < __x10 ^ 2 * __x15 ^ 2 + 2 * __x10 * __x15 * __x14 + __x14 ^ 2) - (H7 : 0 <= __x8) - (H12 : 0 <= __x14) - (H0 : __x8 = __x15 * __x11 + __x9) - (H14 : __x10 ^ 2 * __x15 + __x10 * __x14 < __x16) - (H17 : __x16 <= 0) - (H15 : 0 <= __x9) - (H18 : __x9 < __x15) - (H16 : 0 <= __x12) - (H19 : __x12 < (__x10 * __x15 + __x14) * __x10) + forall (x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 + x14 x15 x16 : Z) + (H6 : x8 < x10 ^ 2 * x15 ^ 2 + 2 * x10 * x15 * x14 + x14 ^ 2) + (H7 : 0 <= x8) + (H12 : 0 <= x14) + (H0 : x8 = x15 * x11 + x9) + (H14 : x10 ^ 2 * x15 + x10 * x14 < x16) + (H17 : x16 <= 0) + (H15 : 0 <= x9) + (H18 : x9 < x15) + (H16 : 0 <= x12) + (H19 : x12 < (x10 * x15 + x14) * x10) , False. Proof. intros. |