Library Coq.Numbers.NatInt.NZMulOrder
Require Import NZAxioms.
Require Import NZAddOrder.
Module NZMulOrderPropFunct (
Import NZOrdAxiomsMod :
NZOrdAxiomsSig).
Module Export NZAddOrderPropMod :=
NZAddOrderPropFunct NZOrdAxiomsMod.
Open Local Scope NatIntScope.
Theorem NZmul_lt_pred :
forall p q n m :
NZ,
S p ==
q -> (
p *
n <
p *
m <->
q *
n +
m <
q *
m +
n).
Theorem NZmul_lt_mono_pos_l :
forall p n m :
NZ, 0 <
p -> (
n <
m <->
p *
n <
p *
m).
Theorem NZmul_lt_mono_pos_r :
forall p n m :
NZ, 0 <
p -> (
n <
m <->
n *
p <
m *
p).
Theorem NZmul_lt_mono_neg_l :
forall p n m :
NZ,
p < 0 -> (
n <
m <->
p *
m <
p *
n).
Theorem NZmul_lt_mono_neg_r :
forall p n m :
NZ,
p < 0 -> (
n <
m <->
m *
p <
n *
p).
Theorem NZmul_le_mono_nonneg_l :
forall n m p :
NZ, 0 <=
p ->
n <=
m ->
p *
n <=
p *
m.
Theorem NZmul_le_mono_nonpos_l :
forall n m p :
NZ,
p <= 0 ->
n <=
m ->
p *
m <=
p *
n.
Theorem NZmul_le_mono_nonneg_r :
forall n m p :
NZ, 0 <=
p ->
n <=
m ->
n *
p <=
m *
p.
Theorem NZmul_le_mono_nonpos_r :
forall n m p :
NZ,
p <= 0 ->
n <=
m ->
m *
p <=
n *
p.
Theorem NZmul_cancel_l :
forall n m p :
NZ,
p ~= 0 -> (
p *
n ==
p *
m <->
n ==
m).
Theorem NZmul_cancel_r :
forall n m p :
NZ,
p ~= 0 -> (
n *
p ==
m *
p <->
n ==
m).
Theorem NZmul_id_l :
forall n m :
NZ,
m ~= 0 -> (
n *
m ==
m <->
n == 1).
Theorem NZmul_id_r :
forall n m :
NZ,
n ~= 0 -> (
n *
m ==
n <->
m == 1).
Theorem NZmul_le_mono_pos_l :
forall n m p :
NZ, 0 <
p -> (
n <=
m <->
p *
n <=
p *
m).
Theorem NZmul_le_mono_pos_r :
forall n m p :
NZ, 0 <
p -> (
n <=
m <->
n *
p <=
m *
p).
Theorem NZmul_le_mono_neg_l :
forall n m p :
NZ,
p < 0 -> (
n <=
m <->
p *
m <=
p *
n).
Theorem NZmul_le_mono_neg_r :
forall n m p :
NZ,
p < 0 -> (
n <=
m <->
m *
p <=
n *
p).
Theorem NZmul_lt_mono_nonneg :
forall n m p q :
NZ, 0 <=
n ->
n <
m -> 0 <=
p ->
p <
q ->
n *
p <
m *
q.
Theorem NZmul_le_mono_nonneg :
forall n m p q :
NZ, 0 <=
n ->
n <=
m -> 0 <=
p ->
p <=
q ->
n *
p <=
m *
q.
Theorem NZmul_pos_pos :
forall n m :
NZ, 0 <
n -> 0 <
m -> 0 <
n *
m.
Theorem NZmul_neg_neg :
forall n m :
NZ,
n < 0 ->
m < 0 -> 0 <
n *
m.
Theorem NZmul_pos_neg :
forall n m :
NZ, 0 <
n ->
m < 0 ->
n *
m < 0.
Theorem NZmul_neg_pos :
forall n m :
NZ,
n < 0 -> 0 <
m ->
n *
m < 0.
Theorem NZlt_1_mul_pos :
forall n m :
NZ, 1 <
n -> 0 <
m -> 1 <
n *
m.
Theorem NZeq_mul_0 :
forall n m :
NZ,
n *
m == 0 <->
n == 0 \/
m == 0.
Theorem NZneq_mul_0 :
forall n m :
NZ,
n ~= 0 /\
m ~= 0 <->
n *
m ~= 0.
Theorem NZeq_square_0 :
forall n :
NZ,
n *
n == 0 <->
n == 0.
Theorem NZeq_mul_0_l :
forall n m :
NZ,
n *
m == 0 ->
m ~= 0 ->
n == 0.
Theorem NZeq_mul_0_r :
forall n m :
NZ,
n *
m == 0 ->
n ~= 0 ->
m == 0.
Theorem NZlt_0_mul :
forall n m :
NZ, 0 <
n *
m <-> (0 <
n /\ 0 <
m) \/ (
m < 0 /\
n < 0).
Theorem NZsquare_lt_mono_nonneg :
forall n m :
NZ, 0 <=
n ->
n <
m ->
n *
n <
m *
m.
Theorem NZsquare_le_mono_nonneg :
forall n m :
NZ, 0 <=
n ->
n <=
m ->
n *
n <=
m *
m.
Theorem NZsquare_lt_simpl_nonneg :
forall n m :
NZ, 0 <=
m ->
n *
n <
m *
m ->
n <
m.
Theorem NZsquare_le_simpl_nonneg :
forall n m :
NZ, 0 <=
m ->
n *
n <=
m *
m ->
n <=
m.
Theorem NZmul_2_mono_l :
forall n m :
NZ,
n <
m -> 1 + (1 + 1) *
n < (1 + 1) *
m.
End NZMulOrderPropFunct.