Library Coq.Numbers.Integer.Abstract.ZMulOrder
Require Export ZAddOrder.
Module Type ZMulOrderProp (
Import Z :
ZAxiomsMiniSig').
Include ZAddOrderProp Z.
Theorem mul_lt_mono_nonpos :
forall n m p q,
m <= 0
-> n < m -> q <= 0
-> p < q -> m * q < n * p.
Theorem mul_le_mono_nonpos :
forall n m p q,
m <= 0
-> n <= m -> q <= 0
-> p <= q -> m * q <= n * p.
Theorem mul_nonpos_nonpos :
forall n m,
n <= 0
-> m <= 0
-> 0
<= n * m.
Theorem mul_nonneg_nonpos :
forall n m, 0
<= n -> m <= 0
-> n * m <= 0.
Theorem mul_nonpos_nonneg :
forall n m,
n <= 0
-> 0
<= m -> n * m <= 0.
Notation mul_pos :=
lt_0_mul (
only parsing).
Theorem lt_mul_0 :
forall n m,
n * m < 0
<-> n < 0
/\ m > 0
\/ n > 0
/\ m < 0.
Notation mul_neg :=
lt_mul_0 (
only parsing).
Theorem le_0_mul :
forall n m, 0
<= n * m -> 0
<= n /\ 0
<= m \/ n <= 0
/\ m <= 0.
Notation mul_nonneg :=
le_0_mul (
only parsing).
Theorem le_mul_0 :
forall n m,
n * m <= 0
-> 0
<= n /\ m <= 0
\/ n <= 0
/\ 0
<= m.
Notation mul_nonpos :=
le_mul_0 (
only parsing).
Notation le_0_square :=
square_nonneg (
only parsing).
Theorem nlt_square_0 :
forall n,
~ n * n < 0.
Theorem square_lt_mono_nonpos :
forall n m,
n <= 0
-> m < n -> n * n < m * m.
Theorem square_le_mono_nonpos :
forall n m,
n <= 0
-> m <= n -> n * n <= m * m.
Theorem square_lt_simpl_nonpos :
forall n m,
m <= 0
-> n * n < m * m -> m < n.
Theorem square_le_simpl_nonpos :
forall n m,
m <= 0
-> n * n <= m * m -> m <= n.
Theorem lt_1_mul_neg :
forall n m,
n < -1
-> m < 0
-> 1
< n * m.
Theorem lt_mul_m1_neg :
forall n m, 1
< n -> m < 0
-> n * m < -1.
Theorem lt_mul_m1_pos :
forall n m,
n < -1
-> 0
< m -> n * m < -1.
Theorem lt_1_mul_l :
forall n m, 1
< n ->
n * m < -1
\/ n * m == 0
\/ 1
< n * m.
Theorem lt_m1_mul_r :
forall n m,
n < -1
->
n * m < -1
\/ n * m == 0
\/ 1
< n * m.
Theorem eq_mul_1 :
forall n m,
n * m == 1
-> n == 1
\/ n == -1.
Theorem lt_mul_diag_l :
forall n m,
n < 0
-> (1
< m <-> n * m < n).
Theorem lt_mul_diag_r :
forall n m, 0
< n -> (1
< m <-> n < n * m).
Theorem le_mul_diag_l :
forall n m,
n < 0
-> (1
<= m <-> n * m <= n).
Theorem le_mul_diag_r :
forall n m, 0
< n -> (1
<= m <-> n <= n * m).
Theorem lt_mul_r :
forall n m p, 0
< n -> 1
< p -> n < m -> n < m * p.
Alternative name :