Library Coq.Numbers.Integer.Abstract.ZMulOrder
Require Export ZAddOrder.
Module ZMulOrderPropFunct (
Import ZAxiomsMod :
ZAxiomsSig).
Module Export ZAddOrderPropMod :=
ZAddOrderPropFunct ZAxiomsMod.
Open Local Scope IntScope.
Theorem Zmul_lt_pred :
forall p q n m :
Z,
S p ==
q -> (
p *
n <
p *
m <->
q *
n +
m <
q *
m +
n).
Theorem Zmul_lt_mono_pos_l :
forall p n m :
Z, 0 <
p -> (
n <
m <->
p *
n <
p *
m).
Theorem Zmul_lt_mono_pos_r :
forall p n m :
Z, 0 <
p -> (
n <
m <->
n *
p <
m *
p).
Theorem Zmul_lt_mono_neg_l :
forall p n m :
Z,
p < 0 -> (
n <
m <->
p *
m <
p *
n).
Theorem Zmul_lt_mono_neg_r :
forall p n m :
Z,
p < 0 -> (
n <
m <->
m *
p <
n *
p).
Theorem Zmul_le_mono_nonneg_l :
forall n m p :
Z, 0 <=
p ->
n <=
m ->
p *
n <=
p *
m.
Theorem Zmul_le_mono_nonpos_l :
forall n m p :
Z,
p <= 0 ->
n <=
m ->
p *
m <=
p *
n.
Theorem Zmul_le_mono_nonneg_r :
forall n m p :
Z, 0 <=
p ->
n <=
m ->
n *
p <=
m *
p.
Theorem Zmul_le_mono_nonpos_r :
forall n m p :
Z,
p <= 0 ->
n <=
m ->
m *
p <=
n *
p.
Theorem Zmul_cancel_l :
forall n m p :
Z,
p ~= 0 -> (
p *
n ==
p *
m <->
n ==
m).
Theorem Zmul_cancel_r :
forall n m p :
Z,
p ~= 0 -> (
n *
p ==
m *
p <->
n ==
m).
Theorem Zmul_id_l :
forall n m :
Z,
m ~= 0 -> (
n *
m ==
m <->
n == 1).
Theorem Zmul_id_r :
forall n m :
Z,
n ~= 0 -> (
n *
m ==
n <->
m == 1).
Theorem Zmul_le_mono_pos_l :
forall n m p :
Z, 0 <
p -> (
n <=
m <->
p *
n <=
p *
m).
Theorem Zmul_le_mono_pos_r :
forall n m p :
Z, 0 <
p -> (
n <=
m <->
n *
p <=
m *
p).
Theorem Zmul_le_mono_neg_l :
forall n m p :
Z,
p < 0 -> (
n <=
m <->
p *
m <=
p *
n).
Theorem Zmul_le_mono_neg_r :
forall n m p :
Z,
p < 0 -> (
n <=
m <->
m *
p <=
n *
p).
Theorem Zmul_lt_mono_nonneg :
forall n m p q :
Z, 0 <=
n ->
n <
m -> 0 <=
p ->
p <
q ->
n *
p <
m *
q.
Theorem Zmul_lt_mono_nonpos :
forall n m p q :
Z,
m <= 0 ->
n <
m ->
q <= 0 ->
p <
q ->
m *
q <
n *
p.
Theorem Zmul_le_mono_nonneg :
forall n m p q :
Z, 0 <=
n ->
n <=
m -> 0 <=
p ->
p <=
q ->
n *
p <=
m *
q.
Theorem Zmul_le_mono_nonpos :
forall n m p q :
Z,
m <= 0 ->
n <=
m ->
q <= 0 ->
p <=
q ->
m *
q <=
n *
p.
Theorem Zmul_pos_pos :
forall n m :
Z, 0 <
n -> 0 <
m -> 0 <
n *
m.
Theorem Zmul_neg_neg :
forall n m :
Z,
n < 0 ->
m < 0 -> 0 <
n *
m.
Theorem Zmul_pos_neg :
forall n m :
Z, 0 <
n ->
m < 0 ->
n *
m < 0.
Theorem Zmul_neg_pos :
forall n m :
Z,
n < 0 -> 0 <
m ->
n *
m < 0.
Theorem Zmul_nonneg_nonneg :
forall n m :
Z, 0 <=
n -> 0 <=
m -> 0 <=
n *
m.
Theorem Zmul_nonpos_nonpos :
forall n m :
Z,
n <= 0 ->
m <= 0 -> 0 <=
n *
m.
Theorem Zmul_nonneg_nonpos :
forall n m :
Z, 0 <=
n ->
m <= 0 ->
n *
m <= 0.
Theorem Zmul_nonpos_nonneg :
forall n m :
Z,
n <= 0 -> 0 <=
m ->
n *
m <= 0.
Theorem Zlt_1_mul_pos :
forall n m :
Z, 1 <
n -> 0 <
m -> 1 <
n *
m.
Theorem Zeq_mul_0 :
forall n m :
Z,
n *
m == 0 <->
n == 0 \/
m == 0.
Theorem Zneq_mul_0 :
forall n m :
Z,
n ~= 0 /\
m ~= 0 <->
n *
m ~= 0.
Theorem Zeq_square_0 :
forall n :
Z,
n *
n == 0 <->
n == 0.
Theorem Zeq_mul_0_l :
forall n m :
Z,
n *
m == 0 ->
m ~= 0 ->
n == 0.
Theorem Zeq_mul_0_r :
forall n m :
Z,
n *
m == 0 ->
n ~= 0 ->
m == 0.
Theorem Zlt_0_mul :
forall n m :
Z, 0 <
n *
m <-> 0 <
n /\ 0 <
m \/
m < 0 /\
n < 0.
Notation Zmul_pos :=
Zlt_0_mul (
only parsing).
Theorem Zlt_mul_0 :
forall n m :
Z,
n *
m < 0 <->
n < 0 /\
m > 0 \/
n > 0 /\
m < 0.
Notation Zmul_neg :=
Zlt_mul_0 (
only parsing).
Theorem Zle_0_mul :
forall n m :
Z, 0 <=
n *
m -> 0 <=
n /\ 0 <=
m \/
n <= 0 /\
m <= 0.
Notation Zmul_nonneg :=
Zle_0_mul (
only parsing).
Theorem Zle_mul_0 :
forall n m :
Z,
n *
m <= 0 -> 0 <=
n /\
m <= 0 \/
n <= 0 /\ 0 <=
m.
Notation Zmul_nonpos :=
Zle_mul_0 (
only parsing).
Theorem Zle_0_square :
forall n :
Z, 0 <=
n *
n.
Notation Zsquare_nonneg :=
Zle_0_square (
only parsing).
Theorem Znlt_square_0 :
forall n :
Z, ~
n *
n < 0.
Theorem Zsquare_lt_mono_nonneg :
forall n m :
Z, 0 <=
n ->
n <
m ->
n *
n <
m *
m.
Theorem Zsquare_lt_mono_nonpos :
forall n m :
Z,
n <= 0 ->
m <
n ->
n *
n <
m *
m.
Theorem Zsquare_le_mono_nonneg :
forall n m :
Z, 0 <=
n ->
n <=
m ->
n *
n <=
m *
m.
Theorem Zsquare_le_mono_nonpos :
forall n m :
Z,
n <= 0 ->
m <=
n ->
n *
n <=
m *
m.
Theorem Zsquare_lt_simpl_nonneg :
forall n m :
Z, 0 <=
m ->
n *
n <
m *
m ->
n <
m.
Theorem Zsquare_le_simpl_nonneg :
forall n m :
Z, 0 <=
m ->
n *
n <=
m *
m ->
n <=
m.
Theorem Zsquare_lt_simpl_nonpos :
forall n m :
Z,
m <= 0 ->
n *
n <
m *
m ->
m <
n.
Theorem Zsquare_le_simpl_nonpos :
forall n m :
NZ,
m <= 0 ->
n *
n <=
m *
m ->
m <=
n.
Theorem Zmul_2_mono_l :
forall n m :
Z,
n <
m -> 1 + (1 + 1) *
n < (1 + 1) *
m.
Theorem Zlt_1_mul_neg :
forall n m :
Z,
n < -1 ->
m < 0 -> 1 <
n *
m.
Theorem Zlt_mul_n1_neg :
forall n m :
Z, 1 <
n ->
m < 0 ->
n *
m < -1.
Theorem Zlt_mul_n1_pos :
forall n m :
Z,
n < -1 -> 0 <
m ->
n *
m < -1.
Theorem Zlt_1_mul_l :
forall n m :
Z, 1 <
n ->
n *
m < -1 \/
n *
m == 0 \/ 1 <
n *
m.
Theorem Zlt_n1_mul_r :
forall n m :
Z,
n < -1 ->
n *
m < -1 \/
n *
m == 0 \/ 1 <
n *
m.
Theorem Zeq_mul_1 :
forall n m :
Z,
n *
m == 1 ->
n == 1 \/
n == -1.
Theorem Zlt_mul_diag_l :
forall n m :
Z,
n < 0 -> (1 <
m <->
n *
m <
n).
Theorem Zlt_mul_diag_r :
forall n m :
Z, 0 <
n -> (1 <
m <->
n <
n *
m).
Theorem Zle_mul_diag_l :
forall n m :
Z,
n < 0 -> (1 <=
m <->
n *
m <=
n).
Theorem Zle_mul_diag_r :
forall n m :
Z, 0 <
n -> (1 <=
m <->
n <=
n *
m).
Theorem Zlt_mul_r :
forall n m p :
Z, 0 <
n -> 1 <
p ->
n <
m ->
n <
m *
p.
End ZMulOrderPropFunct.