# Library Coq.Numbers.Natural.Abstract.NOrder

Require Export NAdd.
Module NOrderPropFunct (Import N : NAxiomsSig').
Include NAddPropFunct N.
Theorem lt_wf_0 : well_founded lt.
Theorem nlt_0_r : forall n, ~ n < 0.
Theorem nle_succ_0 : forall n, ~ (S n <= 0).
Theorem le_0_r : forall n, n <= 0 <-> n == 0.
Theorem lt_0_succ : forall n, 0 < S n.
Theorem neq_0_lt_0 : forall n, n ~= 0 <-> 0 < n.
Theorem eq_0_gt_0_cases : forall n, n == 0 \/ 0 < n.
Theorem zero_one : forall n, n == 0 \/ n == 1 \/ 1 < n.
Theorem lt_1_r : forall n, n < 1 <-> n == 0.
Theorem le_1_r : forall n, n <= 1 <-> n == 0 \/ n == 1.
Theorem lt_lt_0 : forall n m, n < m -> 0 < m.
Theorem lt_1_l' : forall n m p, n < m -> m < p -> 1 < p.
Elimination principlies for < and <= for relations
Section RelElim.
Variable R : relation N.t.
Hypothesis R_wd : Proper (N.eq==>N.eq==>iff) R.
Theorem le_ind_rel :
(forall m, R 0 m) ->
(forall n m, n <= m -> R n m -> R (S n) (S m)) ->
forall n m, n <= m -> R n m.
Theorem lt_ind_rel :
(forall m, R 0 (S m)) ->
(forall n m, n < m -> R n m -> R (S n) (S m)) ->
forall n m, n < m -> R n m.
End RelElim.
Predecessor and order
Theorem succ_pred_pos : forall n, 0 < n -> S (P n) == n.
Theorem le_pred_l : forall n, P n <= n.
Theorem lt_pred_l : forall n, n ~= 0 -> P n < n.
Theorem le_le_pred : forall n m, n <= m -> P n <= m.
Theorem lt_lt_pred : forall n m, n < m -> P n < m.
Theorem lt_le_pred : forall n m, n < m -> n <= P m.
Theorem lt_pred_le : forall n m, P n < m -> n <= m.
Theorem lt_pred_lt : forall n m, n < P m -> n < m.
Theorem le_pred_le : forall n m, n <= P m -> n <= m.
Theorem pred_le_mono : forall n m, n <= m -> P n <= P m.
Theorem pred_lt_mono : forall n m, n ~= 0 -> (n < m <-> P n < P m).
Theorem lt_succ_lt_pred : forall n m, S n < m <-> n < P m.
Theorem le_succ_le_pred : forall n m, S n <= m -> n <= P m.
Theorem lt_pred_lt_succ : forall n m, P n < m -> n < S m.
Theorem le_pred_le_succ : forall n m, P n <= m <-> n <= S m.
End NOrderPropFunct.