Library Coq.Numbers.Natural.Abstract.NAddOrder


Require Export NOrder.

Module NAddOrderProp (Import N : NAxiomsMiniSig').
Include NOrderProp N.

Theorems true for natural numbers, not for integers

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

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

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

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

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

End NAddOrderProp.