Library Coq.Numbers.Natural.Abstract.NOrder



Require Export NMul.

Module NOrderPropFunct (Import NAxiomsMod : NAxiomsSig).
Module Export NMulPropMod := NMulPropFunct NAxiomsMod.
Open Local Scope NatScope.



Theorem lt_wd :
  forall n1 n2 : N, n1 == n2 -> forall m1 m2 : N, m1 == m2 -> (n1 < m1 <-> n2 < m2).
Theorem le_wd :
  forall n1 n2 : N, n1 == n2 -> forall m1 m2 : N, m1 == m2 -> (n1 <= m1 <-> n2 <= m2).
Theorem min_wd :
  forall n1 n2 : N, n1 == n2 -> forall m1 m2 : N, m1 == m2 -> min n1 m1 == min n2 m2.
Theorem max_wd :
  forall n1 n2 : N, n1 == n2 -> forall m1 m2 : N, m1 == m2 -> max n1 m1 == max n2 m2.
Theorem lt_eq_cases : forall n m : N, n <= m <-> n < m \/ n == m.
Theorem lt_irrefl : forall n : N, ~ n < n.
Theorem lt_succ_r : forall n m : N, n < S m <-> n <= m.
Theorem min_l : forall n m : N, n <= m -> min n m == n.
Theorem min_r : forall n m : N, m <= n -> min n m == m.
Theorem max_l : forall n m : N, m <= n -> max n m == n.
Theorem max_r : forall n m : N, n <= m -> max n m == m.
Theorem lt_le_incl : forall n m : N, n < m -> n <= m.
Theorem eq_le_incl : forall n m : N, n == m -> n <= m.
Theorem lt_neq : forall n m : N, n < m -> n ~= m.
Theorem le_neq : forall n m : N, n < m <-> n <= m /\ n ~= m.
Theorem le_refl : forall n : N, n <= n.
Theorem lt_succ_diag_r : forall n : N, n < S n.
Theorem le_succ_diag_r : forall n : N, n <= S n.
Theorem lt_0_1 : 0 < 1.
Theorem le_0_1 : 0 <= 1.
Theorem lt_lt_succ_r : forall n m : N, n < m -> n < S m.
Theorem le_le_succ_r : forall n m : N, n <= m -> n <= S m.
Theorem le_succ_r : forall n m : N, n <= S m <-> n <= m \/ n == S m.
Theorem neq_succ_diag_l : forall n : N, S n ~= n.
Theorem neq_succ_diag_r : forall n : N, n ~= S n.
Theorem nlt_succ_diag_l : forall n : N, ~ S n < n.
Theorem nle_succ_diag_l : forall n : N, ~ S n <= n.
Theorem le_succ_l : forall n m : N, S n <= m <-> n < m.
Theorem lt_succ_l : forall n m : N, S n < m -> n < m.
Theorem succ_lt_mono : forall n m : N, n < m <-> S n < S m.
Theorem succ_le_mono : forall n m : N, n <= m <-> S n <= S m.
Theorem lt_asymm : forall n m : N, n < m -> ~ m < n.
Notation lt_ngt := lt_asymm (only parsing).

Theorem lt_trans : forall n m p : N, n < m -> m < p -> n < p.
Theorem le_trans : forall n m p : N, n <= m -> m <= p -> n <= p.
Theorem le_lt_trans : forall n m p : N, n <= m -> m < p -> n < p.
Theorem lt_le_trans : forall n m p : N, n < m -> m <= p -> n < p.
Theorem le_antisymm : forall n m : N, n <= m -> m <= n -> n == m.
Trichotomy, decidability, and double negation elimination
Theorem lt_trichotomy : forall n m : N, n < m \/ n == m \/ m < n.
Notation lt_eq_gt_cases := lt_trichotomy (only parsing).

Theorem lt_gt_cases : forall n m : N, n ~= m <-> n < m \/ n > m.
Theorem le_gt_cases : forall n m : N, n <= m \/ n > m.
Theorem lt_ge_cases : forall n m : N, n < m \/ n >= m.
Theorem le_ge_cases : forall n m : N, n <= m \/ n >= m.
Theorem le_ngt : forall n m : N, n <= m <-> ~ n > m.
Theorem nlt_ge : forall n m : N, ~ n < m <-> n >= m.
Theorem lt_dec : forall n m : N, decidable (n < m).
Theorem lt_dne : forall n m : N, ~ ~ n < m <-> n < m.
Theorem nle_gt : forall n m : N, ~ n <= m <-> n > m.
Theorem lt_nge : forall n m : N, n < m <-> ~ n >= m.
Theorem le_dec : forall n m : N, decidable (n <= m).
Theorem le_dne : forall n m : N, ~ ~ n <= m <-> n <= m.
Theorem nlt_succ_r : forall n m : N, ~ m < S n <-> n < m.
Theorem lt_exists_pred :
  forall z n : N, z < n -> exists k : N, n == S k /\ z <= k.
Theorem lt_succ_iter_r :
  forall (n : nat) (m : N), m < NZsucc_iter (Datatypes.S n) m.
Theorem neq_succ_iter_l :
  forall (n : nat) (m : N), NZsucc_iter (Datatypes.S n) m ~= m.
Stronger variant of induction with assumptions n >= 0 (n < 0) in the induction step
Theorem right_induction :
  forall A : N -> Prop, predicate_wd Neq A ->
    forall z : N, A z ->
      (forall n : N, z <= n -> A n -> A (S n)) ->
        forall n : N, z <= n -> A n.
Theorem left_induction :
  forall A : N -> Prop, predicate_wd Neq A ->
    forall z : N, A z ->
      (forall n : N, n < z -> A (S n) -> A n) ->
        forall n : N, n <= z -> A n.
Theorem right_induction' :
  forall A : N -> Prop, predicate_wd Neq A ->
    forall z : N,
      (forall n : N, n <= z -> A n) ->
      (forall n : N, z <= n -> A n -> A (S n)) ->
        forall n : N, A n.
Theorem left_induction' :
  forall A : N -> Prop, predicate_wd Neq A ->
    forall z : N,
    (forall n : N, z <= n -> A n) ->
    (forall n : N, n < z -> A (S n) -> A n) ->
      forall n : N, A n.
Theorem strong_right_induction :
  forall A : N -> Prop, predicate_wd Neq A ->
    forall z : N,
    (forall n : N, z <= n -> (forall m : N, z <= m -> m < n -> A m) -> A n) ->
       forall n : N, z <= n -> A n.
Theorem strong_left_induction :
  forall A : N -> Prop, predicate_wd Neq A ->
    forall z : N,
      (forall n : N, n <= z -> (forall m : N, m <= z -> S n <= m -> A m) -> A n) ->
        forall n : N, n <= z -> A n.
Theorem strong_right_induction' :
  forall A : N -> Prop, predicate_wd Neq A ->
    forall z : N,
      (forall n : N, n <= z -> A n) ->
      (forall n : N, z <= n -> (forall m : N, z <= m -> m < n -> A m) -> A n) ->
        forall n : N, A n.
Theorem strong_left_induction' :
  forall A : N -> Prop, predicate_wd Neq A ->
    forall z : N,
    (forall n : N, z <= n -> A n) ->
    (forall n : N, n <= z -> (forall m : N, m <= z -> S n <= m -> A m) -> A n) ->
      forall n : N, A n.
Theorem order_induction :
  forall A : N -> Prop, predicate_wd Neq A ->
    forall z : N, A z ->
      (forall n : N, z <= n -> A n -> A (S n)) ->
      (forall n : N, n < z -> A (S n) -> A n) ->
        forall n : N, A n.
Theorem order_induction' :
  forall A : N -> Prop, predicate_wd Neq A ->
    forall z : N, A z ->
      (forall n : N, z <= n -> A n -> A (S n)) ->
      (forall n : N, n <= z -> A n -> A (P n)) ->
        forall n : N, A n.
Elimintation principle for <
Theorem lt_ind :
  forall A : N -> Prop, predicate_wd Neq A ->
    forall n : N,
      A (S n) ->
      (forall m : N, n < m -> A m -> A (S m)) ->
        forall m : N, n < m -> A m.
Elimintation principle for <=
Theorem le_ind :
  forall A : N -> Prop, predicate_wd Neq A ->
    forall n : N,
      A n ->
      (forall m : N, n <= m -> A m -> A (S m)) ->
        forall m : N, n <= m -> A m.
Well-founded relations
Theorem lt_wf : forall z : N, well_founded (fun n m : N => z <= n /\ n < m).
Theorem gt_wf : forall z : N, well_founded (fun n m : N => m < n /\ n <= z).
Theorem lt_wf_0 : well_founded lt.



Theorem nlt_0_r : forall n : N, ~ n < 0.

Theorem nle_succ_0 : forall n : N, ~ (S n <= 0).

Theorem le_0_r : forall n : N, n <= 0 <-> n == 0.

Theorem lt_0_succ : forall n : N, 0 < S n.

Theorem neq_0_lt_0 : forall n : N, n ~= 0 <-> 0 < n.

Theorem eq_0_gt_0_cases : forall n : N, n == 0 \/ 0 < n.

Theorem zero_one : forall n : N, n == 0 \/ n == 1 \/ 1 < n.

Theorem lt_1_r : forall n : N, n < 1 <-> n == 0.

Theorem le_1_r : forall n : N, n <= 1 <-> n == 0 \/ n == 1.

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

Theorem lt_1_l : forall n m p : N, n < m -> m < p -> 1 < p.

Elimination principlies for < and <= for relations

Section RelElim.


Variable R : N -> N -> Prop.
Hypothesis R_wd : relation_wd Neq Neq R.

Add Morphism R with signature Neq ==> Neq ==> iff as R_morph2.

Theorem le_ind_rel :
   (forall m : N, R 0 m) ->
   (forall n m : N, n <= m -> R n m -> R (S n) (S m)) ->
     forall n m : N, n <= m -> R n m.

Theorem lt_ind_rel :
   (forall m : N, R 0 (S m)) ->
   (forall n m : N, n < m -> R n m -> R (S n) (S m)) ->
   forall n m : N, n < m -> R n m.

End RelElim.

Predecessor and order

Theorem succ_pred_pos : forall n : N, 0 < n -> S (P n) == n.

Theorem le_pred_l : forall n : N, P n <= n.

Theorem lt_pred_l : forall n : N, n ~= 0 -> P n < n.

Theorem le_le_pred : forall n m : N, n <= m -> P n <= m.

Theorem lt_lt_pred : forall n m : N, n < m -> P n < m.

Theorem lt_le_pred : forall n m : N, n < m -> n <= P m.
Theorem lt_pred_le : forall n m : N, P n < m -> n <= m.
Theorem lt_pred_lt : forall n m : N, n < P m -> n < m.

Theorem le_pred_le : forall n m : N, n <= P m -> n <= m.

Theorem pred_le_mono : forall n m : N, n <= m -> P n <= P m.
Theorem pred_lt_mono : forall n m : N, n ~= 0 -> (n < m <-> P n < P m).

Theorem lt_succ_lt_pred : forall n m : N, S n < m <-> n < P m.

Theorem le_succ_le_pred : forall n m : N, S n <= m -> n <= P m.
Theorem lt_pred_lt_succ : forall n m : N, P n < m -> n < S m.
Theorem le_pred_le_succ : forall n m : N, P n <= m <-> n <= S m.

End NOrderPropFunct.