Library Coq.Numbers.Natural.Abstract.NOrder

Require Export NAdd.

Module NOrderProp (Import N : NAxiomsMiniSig').
Include NAddProp 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.

Lemma measure_induction : forall (X : Type) (f : X -> t) (A : X -> Type),
(forall x, (forall y, f y < f x -> A y ) -> A x ) ->
forall x, A x.

End NOrderProp.