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 :