Library Coq.Numbers.Natural.Abstract.NAddOrder



Require Export NOrder.

Module NAddOrderPropFunct (Import NAxiomsMod : NAxiomsSig).
Module Export NOrderPropMod := NOrderPropFunct NAxiomsMod.
Open Local Scope NatScope.

Theorem add_lt_mono_l : forall n m p : N, n < m <-> p + n < p + m.

Theorem add_lt_mono_r : forall n m p : N, n < m <-> n + p < m + p.

Theorem add_lt_mono : forall n m p q : N, n < m -> p < q -> n + p < m + q.

Theorem add_le_mono_l : forall n m p : N, n <= m <-> p + n <= p + m.

Theorem add_le_mono_r : forall n m p : N, n <= m <-> n + p <= m + p.

Theorem add_le_mono : forall n m p q : N, n <= m -> p <= q -> n + p <= m + q.

Theorem add_lt_le_mono : forall n m p q : N, n < m -> p <= q -> n + p < m + q.

Theorem add_le_lt_mono : forall n m p q : N, n <= m -> p < q -> n + p < m + q.

Theorem add_pos_pos : forall n m : N, 0 < n -> 0 < m -> 0 < n + m.

Theorem lt_add_pos_l : forall n m : N, 0 < n -> m < n + m.

Theorem lt_add_pos_r : forall n m : N, 0 < n -> m < m + n.

Theorem le_lt_add_lt : forall n m p q : N, n <= m -> p + m < q + n -> p < q.

Theorem lt_le_add_lt : forall n m p q : N, n < m -> p + m <= q + n -> p < q.

Theorem le_le_add_le : forall n m p q : N, n <= m -> p + m <= q + n -> p <= q.

Theorem add_lt_cases : forall n m p q : N, n + m < p + q -> n < p \/ m < q.

Theorem add_le_cases : forall n m p q : N, n + m <= p + q -> n <= p \/ m <= q.

Theorem add_pos_cases : forall n m : N, 0 < n + m -> 0 < n \/ 0 < m.


Theorem le_add_r : forall n m : N, n <= n + m.


Theorem lt_lt_add_r : forall n m p : N, n < m -> n < m + p.

Theorem lt_lt_add_l : forall n m p : N, n < m -> n < p + m.

Theorem add_pos_l : forall n m : N, 0 < n -> 0 < n + m.


Theorem add_pos_r : forall n m : N, 0 < m -> 0 < n + m.



Theorem add_lt_repl_pair : forall n m n' m' u v : N,
  n + u < m + v -> n + m' == n' + m -> n' + u < m' + v.



End NAddOrderPropFunct.