Library Coq.Numbers.NatInt.NZAddOrder
Require Import NZAxioms NZBase NZMul NZOrder.
Module Type NZAddOrderPropSig (
Import NZ :
NZOrdAxiomsSig').
Include NZBasePropSig NZ <+
NZMulPropSig NZ <+
NZOrderPropSig NZ.
Theorem add_lt_mono_l :
forall n m p,
n < m <-> p + n < p + m.
Theorem add_lt_mono_r :
forall n m p,
n < m <-> n + p < m + p.
Theorem add_lt_mono :
forall n m p q,
n < m ->
p < q ->
n + p < m + q.
Theorem add_le_mono_l :
forall n m p,
n <= m <-> p + n <= p + m.
Theorem add_le_mono_r :
forall n m p,
n <= m <-> n + p <= m + p.
Theorem add_le_mono :
forall n m p q,
n <= m ->
p <= q ->
n + p <= m + q.
Theorem add_lt_le_mono :
forall n m p q,
n < m ->
p <= q ->
n + p < m + q.
Theorem add_le_lt_mono :
forall n m p q,
n <= m ->
p < q ->
n + p < m + q.
Theorem add_pos_pos :
forall n m, 0
< n -> 0
< m -> 0
< n + m.
Theorem add_pos_nonneg :
forall n m, 0
< n -> 0
<= m -> 0
< n + m.
Theorem add_nonneg_pos :
forall n m, 0
<= n -> 0
< m -> 0
< n + m.
Theorem add_nonneg_nonneg :
forall n m, 0
<= n -> 0
<= m -> 0
<= n + m.
Theorem lt_add_pos_l :
forall n m, 0
< n ->
m < n + m.
Theorem lt_add_pos_r :
forall n m, 0
< n ->
m < m + n.
Theorem le_lt_add_lt :
forall n m p q,
n <= m ->
p + m < q + n ->
p < q.
Theorem lt_le_add_lt :
forall n m p q,
n < m ->
p + m <= q + n ->
p < q.
Theorem le_le_add_le :
forall n m p q,
n <= m ->
p + m <= q + n ->
p <= q.
Theorem add_lt_cases :
forall n m p q,
n + m < p + q ->
n < p \/ m < q.
Theorem add_le_cases :
forall n m p q,
n + m <= p + q ->
n <= p \/ m <= q.
Theorem add_neg_cases :
forall n m,
n + m < 0 ->
n < 0
\/ m < 0.
Theorem add_pos_cases :
forall n m, 0
< n + m -> 0
< n \/ 0
< m.
Theorem add_nonpos_cases :
forall n m,
n + m <= 0 ->
n <= 0
\/ m <= 0.
Theorem add_nonneg_cases :
forall n m, 0
<= n + m -> 0
<= n \/ 0
<= m.
End NZAddOrderPropSig.