NOrder.v

Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)
(*                      Evgeny Makarov, INRIA, 2007                     *)
(************************************************************************)

Require Export NAdd.

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

(* Theorems that are true for natural numbers but not for integers *)

Theorem lt_wf_0 : well_founded lt.well_founded lt
Proof.well_founded lt
setoid_replace lt with (fun n m => 0 <= n < m).well_founded (fun n m : t => 0 <= n < m)
relation_equivalence lt (fun n m : t => 0 <= n < m)
apply lt_wf.relation_equivalence lt (fun n m : t => 0 <= n < m)
intros x y; split.x, y:t
x < y -> 0 <= x < y
x, y:t
0 <= x < y -> x < y
intro H; split; [apply le_0_l | assumption].x, y:t
0 <= x < y -> x < y now intros [_ H].
Defined.

(* "le_0_l : forall n : N, 0 <= n" was proved in NBase.v *)

Theorem nlt_0_r : forall n, ~ n < 0.forall n : t, ~ n < 0
Proof.forall n : t, ~ n < 0
intro n; apply le_ngt.n:t
0 <= n apply le_0_l.
Qed.

Theorem nle_succ_0 : forall n, ~ (S n <= 0).forall n : t, ~ S n <= 0
Proof.forall n : t, ~ S n <= 0
intros n H; apply le_succ_l in H; false_hyp H nlt_0_r.
Qed.

Theorem le_0_r : forall n, n <= 0 <-> n == 0.forall n : t, n <= 0 <-> n == 0
Proof.forall n : t, n <= 0 <-> n == 0
intros n; split; intro H.n:t
H:n <= 0
n == 0
n:t
H:n == 0
n <= 0
le_elim H; [false_hyp H nlt_0_r | assumption].n:t
H:n == 0
n <= 0
now apply eq_le_incl.
Qed.

Theorem lt_0_succ : forall n, 0 < S n.forall n : t, 0 < S n
Proof.forall n : t, 0 < S n
induct n; [apply lt_succ_diag_r | intros n H; now apply lt_lt_succ_r].
Qed.

Theorem neq_0_lt_0 : forall n, n ~= 0 <-> 0 < n.forall n : t, n ~= 0 <-> 0 < n
Proof.forall n : t, n ~= 0 <-> 0 < n
cases n.0 ~= 0 <-> 0 < 0
forall n : t, S n ~= 0 <-> 0 < S n
split; intro H; [now elim H | intro; now apply lt_irrefl with 0].forall n : t, S n ~= 0 <-> 0 < S n
intro n; split; intro H; [apply lt_0_succ | apply neq_succ_0].
Qed.

Theorem eq_0_gt_0_cases : forall n, n == 0 \/ 0 < n.forall n : t, n == 0 \/ 0 < n
Proof.forall n : t, n == 0 \/ 0 < n
cases n.0 == 0 \/ 0 < 0
forall n : t, S n == 0 \/ 0 < S n
now left.forall n : t, S n == 0 \/ 0 < S n
intro; right; apply lt_0_succ.
Qed.

Theorem zero_one : forall n, n == 0 \/ n == 1 \/ 1 < n.forall n : t, n == 0 \/ n == 1 \/ 1 < n
Proof.forall n : t, n == 0 \/ n == 1 \/ 1 < n
setoid_rewrite one_succ.forall n : t, n == 0 \/ n == S 0 \/ S 0 < n
induct n.0 == 0 \/ 0 == S 0 \/ S 0 < 0
forall n : t,
n == 0 \/ n == S 0 \/ S 0 < n ->
S n == 0 \/ S n == S 0 \/ S 0 < S n now left.forall n : t,
n == 0 \/ n == S 0 \/ S 0 < n ->
S n == 0 \/ S n == S 0 \/ S 0 < S n
cases n.0 == 0 \/ 0 == S 0 \/ S 0 < 0 ->
S 0 == 0 \/ S 0 == S 0 \/ S 0 < S 0
forall n : t,
S n == 0 \/ S n == S 0 \/ S 0 < S n ->
S (S n) == 0 \/ S (S n) == S 0 \/ S 0 < S (S n) intros; right; now left.forall n : t,
S n == 0 \/ S n == S 0 \/ S 0 < S n ->
S (S n) == 0 \/ S (S n) == S 0 \/ S 0 < S (S n)
intros n IH.n:t
IH:S n == 0 \/ S n == S 0 \/ S 0 < S n
S (S n) == 0 \/ S (S n) == S 0 \/ S 0 < S (S n) destruct IH as [H | [H | H]].n:t
H:S n == 0
S (S n) == 0 \/ S (S n) == S 0 \/ S 0 < S (S n)
n:t
H:S n == S 0
S (S n) == 0 \/ S (S n) == S 0 \/ S 0 < S (S n)
n:t
H:S 0 < S n
S (S n) == 0 \/ S (S n) == S 0 \/ S 0 < S (S n)
false_hyp H neq_succ_0.n:t
H:S n == S 0
S (S n) == 0 \/ S (S n) == S 0 \/ S 0 < S (S n)
n:t
H:S 0 < S n
S (S n) == 0 \/ S (S n) == S 0 \/ S 0 < S (S n)
right; right.n:t
H:S n == S 0
S 0 < S (S n)
n:t
H:S 0 < S n
S (S n) == 0 \/ S (S n) == S 0 \/ S 0 < S (S n) rewrite H.n:t
H:S n == S 0
S 0 < S (S 0)
n:t
H:S 0 < S n
S (S n) == 0 \/ S (S n) == S 0 \/ S 0 < S (S n) apply lt_succ_diag_r.n:t
H:S 0 < S n
S (S n) == 0 \/ S (S n) == S 0 \/ S 0 < S (S n)
right; right.n:t
H:S 0 < S n
S 0 < S (S n) now apply lt_lt_succ_r.
Qed.

Theorem lt_1_r : forall n, n < 1 <-> n == 0.forall n : t, n < 1 <-> n == 0
Proof.forall n : t, n < 1 <-> n == 0
setoid_rewrite one_succ.forall n : t, n < S 0 <-> n == 0
cases n.0 < S 0 <-> 0 == 0
forall n : t, S n < S 0 <-> S n == 0
split; intro; [reflexivity | apply lt_succ_diag_r].forall n : t, S n < S 0 <-> S n == 0
intros n.n:t
S n < S 0 <-> S n == 0 rewrite <- succ_lt_mono.n:t
n < 0 <-> S n == 0
split; intro H; [false_hyp H nlt_0_r | false_hyp H neq_succ_0].
Qed.

Theorem le_1_r : forall n, n <= 1 <-> n == 0 \/ n == 1.forall n : t, n <= 1 <-> n == 0 \/ n == 1
Proof.forall n : t, n <= 1 <-> n == 0 \/ n == 1
setoid_rewrite one_succ.forall n : t, n <= S 0 <-> n == 0 \/ n == S 0
cases n.0 <= S 0 <-> 0 == 0 \/ 0 == S 0
forall n : t, S n <= S 0 <-> S n == 0 \/ S n == S 0
split; intro; [now left | apply le_succ_diag_r].forall n : t, S n <= S 0 <-> S n == 0 \/ S n == S 0
intro n.n:t
S n <= S 0 <-> S n == 0 \/ S n == S 0 rewrite <- succ_le_mono, le_0_r, succ_inj_wd.n:t
n == 0 <-> S n == 0 \/ n == 0
split; [intro; now right | intros [H | H]; [false_hyp H neq_succ_0 | assumption]].
Qed.

Theorem lt_lt_0 : forall n m, n < m -> 0 < m.forall n m : t, n < m -> 0 < m
Proof.forall n m : t, n < m -> 0 < m
intros n m; induct n.m:t
0 < m -> 0 < m
m:t
forall n : t, (n < m -> 0 < m) -> S n < m -> 0 < m
trivial.m:t
forall n : t, (n < m -> 0 < m) -> S n < m -> 0 < m
intros n IH H.m, n:t
IH:n < m -> 0 < m
H:S n < m
0 < m apply IH; now apply lt_succ_l.
Qed.

Theorem lt_1_l' : forall n m p, n < m -> m < p -> 1 < p.forall n m p : t, n < m -> m < p -> 1 < p
Proof.forall n m p : t, n < m -> m < p -> 1 < p
intros.n, m, p:t
H:n < m
H0:m < p
1 < p apply lt_1_l with m; auto.n, m, p:t
H:n < m
H0:m < p
0 < m
apply le_lt_trans with n; auto.n, m, p:t
H:n < m
H0:m < p
0 <= n now apply le_0_l.
Qed.

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.R:relation t
R_wd:Proper (eq ==> eq ==> iff) R
(forall m : t, R 0 m) ->
(forall n m : t, n <= m -> R n m -> R (S n) (S m)) ->
forall n m : t, n <= m -> R n m
Proof.R:relation t
R_wd:Proper (eq ==> eq ==> iff) R
(forall m : t, R 0 m) ->
(forall n m : t, n <= m -> R n m -> R (S n) (S m)) ->
forall n m : t, n <= m -> R n m
intros Base Step; induct n.R:relation t
R_wd:Proper (eq ==> eq ==> iff) R
Base:forall m : t, R 0 m
Step:forall n m : t,
n <= m -> R n m -> R (S n) (S m)
forall m : t, 0 <= m -> R 0 m
R:relation t
R_wd:Proper (eq ==> eq ==> iff) R
Base:forall m : t, R 0 m
Step:forall n m : t,
n <= m -> R n m -> R (S n) (S m)
forall n : t,
(forall m : t, n <= m -> R n m) ->
forall m : t, S n <= m -> R (S n) m
intros; apply Base.R:relation t
R_wd:Proper (eq ==> eq ==> iff) R
Base:forall m : t, R 0 m
Step:forall n m : t,
n <= m -> R n m -> R (S n) (S m)
forall n : t,
(forall m : t, n <= m -> R n m) ->
forall m : t, S n <= m -> R (S n) m
intros n IH m H.R:relation t
R_wd:Proper (eq ==> eq ==> iff) R
Base:forall m0 : t, R 0 m0
Step:forall n0 m0 : t,
n0 <= m0 -> R n0 m0 -> R (S n0) (S m0)
n:t
IH:forall m0 : t, n <= m0 -> R n m0
m:t
H:S n <= m
R (S n) m elim H using le_ind.R:relation t
R_wd:Proper (eq ==> eq ==> iff) R
Base:forall m0 : t, R 0 m0
Step:forall n0 m0 : t,
n0 <= m0 -> R n0 m0 -> R (S n0) (S m0)
n:t
IH:forall m0 : t, n <= m0 -> R n m0
m:t
H:S n <= m
Proper (eq ==> iff) (fun m0 : t => R (S n) m0)
R:relation t
R_wd:Proper (eq ==> eq ==> iff) R
Base:forall m0 : t, R 0 m0
Step:forall n0 m0 : t,
n0 <= m0 -> R n0 m0 -> R (S n0) (S m0)
n:t
IH:forall m0 : t, n <= m0 -> R n m0
m:t
H:S n <= m
R (S n) (S n)
R:relation t
R_wd:Proper (eq ==> eq ==> iff) R
Base:forall m0 : t, R 0 m0
Step:forall n0 m0 : t,
n0 <= m0 -> R n0 m0 -> R (S n0) (S m0)
n:t
IH:forall m0 : t, n <= m0 -> R n m0
m:t
H:S n <= m
forall m0 : t,
S n <= m0 -> R (S n) m0 -> R (S n) (S m0)
solve_proper.R:relation t
R_wd:Proper (eq ==> eq ==> iff) R
Base:forall m0 : t, R 0 m0
Step:forall n0 m0 : t,
n0 <= m0 -> R n0 m0 -> R (S n0) (S m0)
n:t
IH:forall m0 : t, n <= m0 -> R n m0
m:t
H:S n <= m
R (S n) (S n)
R:relation t
R_wd:Proper (eq ==> eq ==> iff) R
Base:forall m0 : t, R 0 m0
Step:forall n0 m0 : t,
n0 <= m0 -> R n0 m0 -> R (S n0) (S m0)
n:t
IH:forall m0 : t, n <= m0 -> R n m0
m:t
H:S n <= m
forall m0 : t,
S n <= m0 -> R (S n) m0 -> R (S n) (S m0)
apply Step; [| apply IH]; now apply eq_le_incl.R:relation t
R_wd:Proper (eq ==> eq ==> iff) R
Base:forall m0 : t, R 0 m0
Step:forall n0 m0 : t,
n0 <= m0 -> R n0 m0 -> R (S n0) (S m0)
n:t
IH:forall m0 : t, n <= m0 -> R n m0
m:t
H:S n <= m
forall m0 : t,
S n <= m0 -> R (S n) m0 -> R (S n) (S m0)
intros k H1 H2.R:relation t
R_wd:Proper (eq ==> eq ==> iff) R
Base:forall m0 : t, R 0 m0
Step:forall n0 m0 : t,
n0 <= m0 -> R n0 m0 -> R (S n0) (S m0)
n:t
IH:forall m0 : t, n <= m0 -> R n m0
m:t
H:S n <= m
k:t
H1:S n <= k
H2:R (S n) k
R (S n) (S k) apply le_succ_l in H1.R:relation t
R_wd:Proper (eq ==> eq ==> iff) R
Base:forall m0 : t, R 0 m0
Step:forall n0 m0 : t,
n0 <= m0 -> R n0 m0 -> R (S n0) (S m0)
n:t
IH:forall m0 : t, n <= m0 -> R n m0
m:t
H:S n <= m
k:t
H1:n < k
H2:R (S n) k
R (S n) (S k) apply lt_le_incl in H1.R:relation t
R_wd:Proper (eq ==> eq ==> iff) R
Base:forall m0 : t, R 0 m0
Step:forall n0 m0 : t,
n0 <= m0 -> R n0 m0 -> R (S n0) (S m0)
n:t
IH:forall m0 : t, n <= m0 -> R n m0
m:t
H:S n <= m
k:t
H1:n <= k
H2:R (S n) k
R (S n) (S k) auto.
Qed.

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.R:relation t
R_wd:Proper (eq ==> eq ==> iff) R
(forall m : t, R 0 (S m)) ->
(forall n m : t, n < m -> R n m -> R (S n) (S m)) ->
forall n m : t, n < m -> R n m
Proof.R:relation t
R_wd:Proper (eq ==> eq ==> iff) R
(forall m : t, R 0 (S m)) ->
(forall n m : t, n < m -> R n m -> R (S n) (S m)) ->
forall n m : t, n < m -> R n m
intros Base Step; induct n.R:relation t
R_wd:Proper (eq ==> eq ==> iff) R
Base:forall m : t, R 0 (S m)
Step:forall n m : t, n < m -> R n m -> R (S n) (S m)
forall m : t, 0 < m -> R 0 m
R:relation t
R_wd:Proper (eq ==> eq ==> iff) R
Base:forall m : t, R 0 (S m)
Step:forall n m : t, n < m -> R n m -> R (S n) (S m)
forall n : t,
(forall m : t, n < m -> R n m) ->
forall m : t, S n < m -> R (S n) m
intros m H.R:relation t
R_wd:Proper (eq ==> eq ==> iff) R
Base:forall m0 : t, R 0 (S m0)
Step:forall n m0 : t,
n < m0 -> R n m0 -> R (S n) (S m0)
m:t
H:0 < m
R 0 m
R:relation t
R_wd:Proper (eq ==> eq ==> iff) R
Base:forall m : t, R 0 (S m)
Step:forall n m : t, n < m -> R n m -> R (S n) (S m)
forall n : t,
(forall m : t, n < m -> R n m) ->
forall m : t, S n < m -> R (S n) m apply lt_exists_pred in H; destruct H as [m' [H _]].R:relation t
R_wd:Proper (eq ==> eq ==> iff) R
Base:forall m0 : t, R 0 (S m0)
Step:forall n m0 : t,
n < m0 -> R n m0 -> R (S n) (S m0)
m, m':t
H:m == S m'
R 0 m
R:relation t
R_wd:Proper (eq ==> eq ==> iff) R
Base:forall m : t, R 0 (S m)
Step:forall n m : t, n < m -> R n m -> R (S n) (S m)
forall n : t,
(forall m : t, n < m -> R n m) ->
forall m : t, S n < m -> R (S n) m
rewrite H; apply Base.R:relation t
R_wd:Proper (eq ==> eq ==> iff) R
Base:forall m : t, R 0 (S m)
Step:forall n m : t, n < m -> R n m -> R (S n) (S m)
forall n : t,
(forall m : t, n < m -> R n m) ->
forall m : t, S n < m -> R (S n) m
intros n IH m H.R:relation t
R_wd:Proper (eq ==> eq ==> iff) R
Base:forall m0 : t, R 0 (S m0)
Step:forall n0 m0 : t,
n0 < m0 -> R n0 m0 -> R (S n0) (S m0)
n:t
IH:forall m0 : t, n < m0 -> R n m0
m:t
H:S n < m
R (S n) m elim H using lt_ind.R:relation t
R_wd:Proper (eq ==> eq ==> iff) R
Base:forall m0 : t, R 0 (S m0)
Step:forall n0 m0 : t,
n0 < m0 -> R n0 m0 -> R (S n0) (S m0)
n:t
IH:forall m0 : t, n < m0 -> R n m0
m:t
H:S n < m
Proper (eq ==> iff) (fun m0 : t => R (S n) m0)
R:relation t
R_wd:Proper (eq ==> eq ==> iff) R
Base:forall m0 : t, R 0 (S m0)
Step:forall n0 m0 : t,
n0 < m0 -> R n0 m0 -> R (S n0) (S m0)
n:t
IH:forall m0 : t, n < m0 -> R n m0
m:t
H:S n < m
R (S n) (S (S n))
R:relation t
R_wd:Proper (eq ==> eq ==> iff) R
Base:forall m0 : t, R 0 (S m0)
Step:forall n0 m0 : t,
n0 < m0 -> R n0 m0 -> R (S n0) (S m0)
n:t
IH:forall m0 : t, n < m0 -> R n m0
m:t
H:S n < m
forall m0 : t,
S n < m0 -> R (S n) m0 -> R (S n) (S m0)
solve_proper.R:relation t
R_wd:Proper (eq ==> eq ==> iff) R
Base:forall m0 : t, R 0 (S m0)
Step:forall n0 m0 : t,
n0 < m0 -> R n0 m0 -> R (S n0) (S m0)
n:t
IH:forall m0 : t, n < m0 -> R n m0
m:t
H:S n < m
R (S n) (S (S n))
R:relation t
R_wd:Proper (eq ==> eq ==> iff) R
Base:forall m0 : t, R 0 (S m0)
Step:forall n0 m0 : t,
n0 < m0 -> R n0 m0 -> R (S n0) (S m0)
n:t
IH:forall m0 : t, n < m0 -> R n m0
m:t
H:S n < m
forall m0 : t,
S n < m0 -> R (S n) m0 -> R (S n) (S m0)
apply Step; [| apply IH]; now apply lt_succ_diag_r.R:relation t
R_wd:Proper (eq ==> eq ==> iff) R
Base:forall m0 : t, R 0 (S m0)
Step:forall n0 m0 : t,
n0 < m0 -> R n0 m0 -> R (S n0) (S m0)
n:t
IH:forall m0 : t, n < m0 -> R n m0
m:t
H:S n < m
forall m0 : t,
S n < m0 -> R (S n) m0 -> R (S n) (S m0)
intros k H1 H2.R:relation t
R_wd:Proper (eq ==> eq ==> iff) R
Base:forall m0 : t, R 0 (S m0)
Step:forall n0 m0 : t,
n0 < m0 -> R n0 m0 -> R (S n0) (S m0)
n:t
IH:forall m0 : t, n < m0 -> R n m0
m:t
H:S n < m
k:t
H1:S n < k
H2:R (S n) k
R (S n) (S k) apply lt_succ_l in H1.R:relation t
R_wd:Proper (eq ==> eq ==> iff) R
Base:forall m0 : t, R 0 (S m0)
Step:forall n0 m0 : t,
n0 < m0 -> R n0 m0 -> R (S n0) (S m0)
n:t
IH:forall m0 : t, n < m0 -> R n m0
m:t
H:S n < m
k:t
H1:n < k
H2:R (S n) k
R (S n) (S k) auto.
Qed.

End RelElim.

Predecessor and order

Theorem succ_pred_pos : forall n, 0 < n -> S (P n) == n.forall n : t, 0 < n -> S (P n) == n
Proof.forall n : t, 0 < n -> S (P n) == n
intros n H; apply succ_pred; intro H1; rewrite H1 in H.n:t
H:0 < 0
H1:n == 0
False
false_hyp H lt_irrefl.
Qed.

Theorem le_pred_l : forall n, P n <= n.forall n : t, P n <= n
Proof.forall n : t, P n <= n
cases n.P 0 <= 0
forall n : t, P (S n) <= S n
rewrite pred_0; now apply eq_le_incl.forall n : t, P (S n) <= S n
intros; rewrite pred_succ;  apply le_succ_diag_r.
Qed.

Theorem lt_pred_l : forall n, n ~= 0 -> P n < n.forall n : t, n ~= 0 -> P n < n
Proof.forall n : t, n ~= 0 -> P n < n
cases n.0 ~= 0 -> P 0 < 0
forall n : t, S n ~= 0 -> P (S n) < S n
intro H; exfalso; now apply H.forall n : t, S n ~= 0 -> P (S n) < S n
intros; rewrite pred_succ;  apply lt_succ_diag_r.
Qed.

Theorem le_le_pred : forall n m, n <= m -> P n <= m.forall n m : t, n <= m -> P n <= m
Proof.forall n m : t, n <= m -> P n <= m
intros n m H; apply le_trans with n.n, m:t
H:n <= m
P n <= n
n, m:t
H:n <= m
n <= m apply le_pred_l.n, m:t
H:n <= m
n <= m assumption.
Qed.

Theorem lt_lt_pred : forall n m, n < m -> P n < m.forall n m : t, n < m -> P n < m
Proof.forall n m : t, n < m -> P n < m
intros n m H; apply le_lt_trans with n.n, m:t
H:n < m
P n <= n
n, m:t
H:n < m
n < m apply le_pred_l.n, m:t
H:n < m
n < m assumption.
Qed.

Theorem lt_le_pred : forall n m, n < m -> n <= P m.forall n m : t, n < m -> n <= P m
 (* Converse is false for n == m == 0 *)
Proof.forall n m : t, n < m -> n <= P m
intro n; cases m.n:t
n < 0 -> n <= P 0
n:t
forall n0 : t, n < S n0 -> n <= P (S n0)
intro H; false_hyp H nlt_0_r.n:t
forall n0 : t, n < S n0 -> n <= P (S n0)
intros m IH.n, m:t
IH:n < S m
n <= P (S m) rewrite pred_succ; now apply lt_succ_r.
Qed.

Theorem lt_pred_le : forall n m, P n < m -> n <= m.forall n m : t, P n < m -> n <= m
 (* Converse is false for n == m == 0 *)
Proof.forall n m : t, P n < m -> n <= m
intros n m; cases n.m:t
P 0 < m -> 0 <= m
m:t
forall n : t, P (S n) < m -> S n <= m
rewrite pred_0; intro H; now apply lt_le_incl.m:t
forall n : t, P (S n) < m -> S n <= m
intros n IH.m, n:t
IH:P (S n) < m
S n <= m rewrite pred_succ in IH.m, n:t
IH:n < m
S n <= m now apply le_succ_l.
Qed.

Theorem lt_pred_lt : forall n m, n < P m -> n < m.forall n m : t, n < P m -> n < m
Proof.forall n m : t, n < P m -> n < m
intros n m H; apply lt_le_trans with (P m); [assumption | apply le_pred_l].
Qed.

Theorem le_pred_le : forall n m, n <= P m -> n <= m.forall n m : t, n <= P m -> n <= m
Proof.forall n m : t, n <= P m -> n <= m
intros n m H; apply le_trans with (P m); [assumption | apply le_pred_l].
Qed.

Theorem pred_le_mono : forall n m, n <= m -> P n <= P m.forall n m : t, n <= m -> P n <= P m
 (* Converse is false for n == 1, m == 0 *)
Proof.forall n m : t, n <= m -> P n <= P m
intros n m H; elim H using le_ind_rel.n, m:t
H:n <= m
Proper (eq ==> eq ==> iff)
  (fun n0 m0 : t => P n0 <= P m0)
n, m:t
H:n <= m
forall m0 : t, P 0 <= P m0
n, m:t
H:n <= m
forall n0 m0 : t,
n0 <= m0 -> P n0 <= P m0 -> P (S n0) <= P (S m0)
solve_proper.n, m:t
H:n <= m
forall m0 : t, P 0 <= P m0
n, m:t
H:n <= m
forall n0 m0 : t,
n0 <= m0 -> P n0 <= P m0 -> P (S n0) <= P (S m0)
intro; rewrite pred_0; apply le_0_l.n, m:t
H:n <= m
forall n0 m0 : t,
n0 <= m0 -> P n0 <= P m0 -> P (S n0) <= P (S m0)
intros p q H1 _; now do 2 rewrite pred_succ.
Qed.

Theorem pred_lt_mono : forall n m, n ~= 0 -> (n < m <-> P n < P m).forall n m : t, n ~= 0 -> n < m <-> P n < P m
Proof.forall n m : t, n ~= 0 -> n < m <-> P n < P m
intros n m H1; split; intro H2.n, m:t
H1:n ~= 0
H2:n < m
P n < P m
n, m:t
H1:n ~= 0
H2:P n < P m
n < m
assert (m ~= 0).n, m:t
H1:n ~= 0
H2:n < m
m ~= 0
n, m:t
H1:n ~= 0
H2:n < m
H:m ~= 0
P n < P m
n, m:t
H1:n ~= 0
H2:P n < P m
n < m apply neq_0_lt_0.n, m:t
H1:n ~= 0
H2:n < m
0 < m
n, m:t
H1:n ~= 0
H2:n < m
H:m ~= 0
P n < P m
n, m:t
H1:n ~= 0
H2:P n < P m
n < m now apply lt_lt_0 with n.n, m:t
H1:n ~= 0
H2:n < m
H:m ~= 0
P n < P m
n, m:t
H1:n ~= 0
H2:P n < P m
n < m
now rewrite <- (succ_pred n) in H2; rewrite <- (succ_pred m) in H2 ;
[apply succ_lt_mono | | |].n, m:t
H1:n ~= 0
H2:P n < P m
n < m
assert (m ~= 0).n, m:t
H1:n ~= 0
H2:P n < P m
m ~= 0
n, m:t
H1:n ~= 0
H2:P n < P m
H:m ~= 0
n < m apply neq_0_lt_0.n, m:t
H1:n ~= 0
H2:P n < P m
0 < m
n, m:t
H1:n ~= 0
H2:P n < P m
H:m ~= 0
n < m apply lt_lt_0 with (P n).n, m:t
H1:n ~= 0
H2:P n < P m
P n < m
n, m:t
H1:n ~= 0
H2:P n < P m
H:m ~= 0
n < m
apply lt_le_trans with (P m).n, m:t
H1:n ~= 0
H2:P n < P m
P n < P m
n, m:t
H1:n ~= 0
H2:P n < P m
P m <= m
n, m:t
H1:n ~= 0
H2:P n < P m
H:m ~= 0
n < m assumption.n, m:t
H1:n ~= 0
H2:P n < P m
P m <= m
n, m:t
H1:n ~= 0
H2:P n < P m
H:m ~= 0
n < m apply le_pred_l.n, m:t
H1:n ~= 0
H2:P n < P m
H:m ~= 0
n < m
apply succ_lt_mono in H2.n, m:t
H1:n ~= 0
H2:S (P n) < S (P m)
H:m ~= 0
n < m now do 2 rewrite succ_pred in H2.
Qed.

Theorem lt_succ_lt_pred : forall n m, S n < m <-> n < P m.forall n m : t, S n < m <-> n < P m
Proof.forall n m : t, S n < m <-> n < P m
intros n m.n, m:t
S n < m <-> n < P m rewrite pred_lt_mono by apply neq_succ_0.n, m:t
P (S n) < P m <-> n < P m now rewrite pred_succ.
Qed.

Theorem le_succ_le_pred : forall n m, S n <= m -> n <= P m.forall n m : t, S n <= m -> n <= P m
 (* Converse is false for n == m == 0 *)
Proof.forall n m : t, S n <= m -> n <= P m
intros n m H.n, m:t
H:S n <= m
n <= P m apply lt_le_pred.n, m:t
H:S n <= m
n < m now apply le_succ_l.
Qed.

Theorem lt_pred_lt_succ : forall n m, P n < m -> n < S m.forall n m : t, P n < m -> n < S m
 (* Converse is false for n == m == 0 *)
Proof.forall n m : t, P n < m -> n < S m
intros n m H.n, m:t
H:P n < m
n < S m apply lt_succ_r.n, m:t
H:P n < m
n <= m now apply lt_pred_le.
Qed.

Theorem le_pred_le_succ : forall n m, P n <= m <-> n <= S m.forall n m : t, P n <= m <-> n <= S m
Proof.forall n m : t, P n <= m <-> n <= S m
intros n m; cases n.m:t
P 0 <= m <-> 0 <= S m
m:t
forall n : t, P (S n) <= m <-> S n <= S m
rewrite pred_0.m:t
0 <= m <-> 0 <= S m
m:t
forall n : t, P (S n) <= m <-> S n <= S m split; intro H; apply le_0_l.m:t
forall n : t, P (S n) <= m <-> S n <= S m
intro n.m, n:t
P (S n) <= m <-> S n <= S m rewrite pred_succ.m, n:t
n <= m <-> S n <= S m apply succ_le_mono.
Qed.

End NOrderProp.