diff options
Diffstat (limited to 'theories/Numbers/Integer/Abstract/ZMulOrder.v')
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZMulOrder.v | 9 |
1 files changed, 1 insertions, 8 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZMulOrder.v b/theories/Numbers/Integer/Abstract/ZMulOrder.v index 25989b2d4..1010a0f2f 100644 --- a/theories/Numbers/Integer/Abstract/ZMulOrder.v +++ b/theories/Numbers/Integer/Abstract/ZMulOrder.v @@ -92,14 +92,7 @@ Qed. Notation mul_nonpos := le_mul_0 (only parsing). -Theorem le_0_square : forall n, 0 <= n * n. -Proof. -intro n; destruct (neg_nonneg_cases n). -apply lt_le_incl; now apply mul_neg_neg. -now apply mul_nonneg_nonneg. -Qed. - -Notation square_nonneg := le_0_square (only parsing). +Notation le_0_square := square_nonneg (only parsing). Theorem nlt_square_0 : forall n, ~ n * n < 0. Proof. |