NZOrder.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 Import NZAxioms NZBase Decidable OrdersTac.

Module Type NZOrderProp
 (Import NZ : NZOrdSig')(Import NZBase : NZBaseProp NZ).

Instance le_wd : Proper (eq==>eq==>iff) le.Proper (eq ==> eq ==> iff) le
Proof.Proper (eq ==> eq ==> iff) le
intros n n' Hn m m' Hm.n, n':t
Hn:n == n'
m, m':t
Hm:m == m'
n <= m <-> n' <= m' now rewrite <- !lt_succ_r, Hn, Hm.
Qed.

Ltac le_elim H := rewrite lt_eq_cases in H; destruct H as [H | H].

Theorem lt_le_incl : forall n m, n < m -> n <= m.forall n m : t, n < m -> n <= m
Proof.forall n m : t, n < m -> n <= m
intros.n, m:t
H:n < m
n <= m apply lt_eq_cases.n, m:t
H:n < m
n < m \/ n == m now left.
Qed.

Theorem le_refl : forall n, n <= n.forall n : t, n <= n
Proof.forall n : t, n <= n
intro.n:t
n <= n apply lt_eq_cases.n:t
n < n \/ n == n now right.
Qed.

Theorem lt_succ_diag_r : forall n, n < S n.forall n : t, n < S n
Proof.forall n : t, n < S n
intro n.n:t
n < S n rewrite lt_succ_r.n:t
n <= n apply le_refl.
Qed.

Theorem le_succ_diag_r : forall n, n <= S n.forall n : t, n <= S n
Proof.forall n : t, n <= S n
intro; apply lt_le_incl; apply lt_succ_diag_r.
Qed.

Theorem neq_succ_diag_l : forall n, S n ~= n.forall n : t, S n ~= n
Proof.forall n : t, S n ~= n
intros n H.n:t
H:S n == n
False apply (lt_irrefl n).n:t
H:S n == n
n < n rewrite <- H at 2.n:t
H:S n == n
n < S n apply lt_succ_diag_r.
Qed.

Theorem neq_succ_diag_r : forall n, n ~= S n.forall n : t, n ~= S n
Proof.forall n : t, n ~= S n
intro n; apply neq_sym, neq_succ_diag_l.
Qed.

Theorem nlt_succ_diag_l : forall n, ~ S n < n.forall n : t, ~ S n < n
Proof.forall n : t, ~ S n < n
intros n H.n:t
H:S n < n
False apply (lt_irrefl (S n)).n:t
H:S n < n
S n < S n rewrite lt_succ_r.n:t
H:S n < n
S n <= n now apply lt_le_incl.
Qed.

Theorem nle_succ_diag_l : forall n, ~ S n <= n.forall n : t, ~ S n <= n
Proof.forall n : t, ~ S n <= n
intros n H; le_elim H.n:t
H:S n < n
False
n:t
H:S n == n
False
+n:t
H:S n < n
False false_hyp H nlt_succ_diag_l. +n:t
H:S n == n
False false_hyp H neq_succ_diag_l.
Qed.

Theorem le_succ_l : forall n m, S n <= m <-> n < m.forall n m : t, S n <= m <-> n < m
Proof.forall n m : t, S n <= m <-> n < m
intro n; nzinduct m n.n:t
S n <= n <-> n < n
n:t
forall n0 : t,
(S n <= n0 <-> n < n0) <-> (S n <= S n0 <-> n < S n0)
-n:t
S n <= n <-> n < n split; intro H.n:t
H:S n <= n
n < n
n:t
H:n < n
S n <= n +n:t
H:S n <= n
n < n false_hyp H nle_succ_diag_l. +n:t
H:n < n
S n <= n false_hyp H lt_irrefl.
-n:t
forall n0 : t,
(S n <= n0 <-> n < n0) <-> (S n <= S n0 <-> n < S n0) intro m.n, m:t
(S n <= m <-> n < m) <-> (S n <= S m <-> n < S m)
  rewrite (lt_eq_cases (S n) (S m)), !lt_succ_r, (lt_eq_cases n m), succ_inj_wd.n, m:t
(S n <= m <-> n < m) <->
(S n <= m \/ n == m <-> n < m \/ n == m)
  rewrite or_cancel_r.n, m:t
(S n <= m <-> n < m) <-> (S n <= m <-> n < m)
n, m:t
S n <= m -> n ~= m
n, m:t
n < m -> n ~= m
  +n, m:t
(S n <= m <-> n < m) <-> (S n <= m <-> n < m) reflexivity.
  +n, m:t
S n <= m -> n ~= m intros LE EQ; rewrite EQ in LE; false_hyp LE nle_succ_diag_l.
  +n, m:t
n < m -> n ~= m intros LT EQ; rewrite EQ in LT; false_hyp LT lt_irrefl.
Qed.

Trichotomy

Theorem le_gt_cases : forall n m, n <= m \/ n > m.forall n m : t, n <= m \/ m < n
Proof.forall n m : t, n <= m \/ m < n
intros n m; nzinduct n m.m:t
m <= m \/ m < m
m:t
forall n : t, n <= m \/ m < n <-> S n <= m \/ m < S n
-m:t
m <= m \/ m < m left; apply le_refl.
-m:t
forall n : t, n <= m \/ m < n <-> S n <= m \/ m < S n intro n.m, n:t
n <= m \/ m < n <-> S n <= m \/ m < S n rewrite lt_succ_r, le_succ_l, !lt_eq_cases.m, n:t
(n < m \/ n == m) \/ m < n <->
n < m \/ m < n \/ m == n intuition.
Qed.

Theorem lt_trichotomy : forall n m,  n < m \/ n == m \/ m < n.forall n m : t, n < m \/ n == m \/ m < n
Proof.forall n m : t, n < m \/ n == m \/ m < n
intros n m.n, m:t
n < m \/ n == m \/ m < n generalize (le_gt_cases n m); rewrite lt_eq_cases; tauto.
Qed.

Notation lt_eq_gt_cases := lt_trichotomy (only parsing).

Asymmetry and transitivity.

Theorem lt_asymm : forall n m, n < m -> ~ m < n.forall n m : t, n < m -> ~ m < n
Proof.forall n m : t, n < m -> ~ m < n
intros n m; nzinduct n m.m:t
m < m -> ~ m < m
m:t
forall n : t,
(n < m -> ~ m < n) <-> (S n < m -> ~ m < S n)
-m:t
m < m -> ~ m < m intros H; false_hyp H lt_irrefl.
-m:t
forall n : t,
(n < m -> ~ m < n) <-> (S n < m -> ~ m < S n) intro n; split; intros H H1 H2.m, n:t
H:n < m -> ~ m < n
H1:S n < m
H2:m < S n
False
m, n:t
H:S n < m -> ~ m < S n
H1:n < m
H2:m < n
False
  +m, n:t
H:n < m -> ~ m < n
H1:S n < m
H2:m < S n
False apply lt_succ_r in H2.m, n:t
H:n < m -> ~ m < n
H1:S n < m
H2:m <= n
False le_elim H2.m, n:t
H:n < m -> ~ m < n
H1:S n < m
H2:m < n
False
m, n:t
H:n < m -> ~ m < n
H1:S n < m
H2:m == n
False
    *m, n:t
H:n < m -> ~ m < n
H1:S n < m
H2:m < n
False apply H; auto.m, n:t
H:n < m -> ~ m < n
H1:S n < m
H2:m < n
n < m apply le_succ_l.m, n:t
H:n < m -> ~ m < n
H1:S n < m
H2:m < n
S n <= m now apply lt_le_incl.
    *m, n:t
H:n < m -> ~ m < n
H1:S n < m
H2:m == n
False rewrite H2 in H1.m, n:t
H:n < m -> ~ m < n
H1:S n < n
H2:m == n
False false_hyp H1 nlt_succ_diag_l.
  +m, n:t
H:S n < m -> ~ m < S n
H1:n < m
H2:m < n
False apply le_succ_l in H1.m, n:t
H:S n < m -> ~ m < S n
H1:S n <= m
H2:m < n
False le_elim H1.m, n:t
H:S n < m -> ~ m < S n
H1:S n < m
H2:m < n
False
m, n:t
H:S n < m -> ~ m < S n
H1:S n == m
H2:m < n
False
    *m, n:t
H:S n < m -> ~ m < S n
H1:S n < m
H2:m < n
False apply H; auto.m, n:t
H:S n < m -> ~ m < S n
H1:S n < m
H2:m < n
m < S n rewrite lt_succ_r.m, n:t
H:S n < m -> ~ m < S n
H1:S n < m
H2:m < n
m <= n now apply lt_le_incl.
    *m, n:t
H:S n < m -> ~ m < S n
H1:S n == m
H2:m < n
False rewrite <- H1 in H2.m, n:t
H:S n < m -> ~ m < S n
H1:S n == m
H2:S n < n
False false_hyp H2 nlt_succ_diag_l.
Qed.

Notation lt_ngt := lt_asymm (only parsing).

Theorem lt_trans : forall n m p, n < m -> m < p -> n < p.forall n m p : t, n < m -> m < p -> n < p
Proof.forall n m p : t, n < m -> m < p -> n < p
intros n m p; nzinduct p m.n, m:t
n < m -> m < m -> n < m
n, m:t
forall n0 : t,
(n < m -> m < n0 -> n < n0) <->
(n < m -> m < S n0 -> n < S n0)
-n, m:t
n < m -> m < m -> n < m intros _ H; false_hyp H lt_irrefl.
-n, m:t
forall n0 : t,
(n < m -> m < n0 -> n < n0) <->
(n < m -> m < S n0 -> n < S n0) intro p.n, m, p:t
(n < m -> m < p -> n < p) <->
(n < m -> m < S p -> n < S p) rewrite 2 lt_succ_r.n, m, p:t
(n < m -> m < p -> n < p) <->
(n < m -> m <= p -> n <= p)
  split; intros H H1 H2.n, m, p:t
H:n < m -> m < p -> n < p
H1:n < m
H2:m <= p
n <= p
n, m, p:t
H:n < m -> m <= p -> n <= p
H1:n < m
H2:m < p
n < p
  +n, m, p:t
H:n < m -> m < p -> n < p
H1:n < m
H2:m <= p
n <= p apply lt_le_incl; le_elim H2; [now apply H | now rewrite H2 in H1].
  +n, m, p:t
H:n < m -> m <= p -> n <= p
H1:n < m
H2:m < p
n < p assert (n <= p) as H3 by (auto using lt_le_incl).n, m, p:t
H:n < m -> m <= p -> n <= p
H1:n < m
H2:m < p
H3:n <= p
n < p
    le_elim H3.n, m, p:t
H:n < m -> m <= p -> n <= p
H1:n < m
H2:m < p
H3:n < p
n < p
n, m, p:t
H:n < m -> m <= p -> n <= p
H1:n < m
H2:m < p
H3:n == p
n < p
    *n, m, p:t
H:n < m -> m <= p -> n <= p
H1:n < m
H2:m < p
H3:n < p
n < p assumption.
    *n, m, p:t
H:n < m -> m <= p -> n <= p
H1:n < m
H2:m < p
H3:n == p
n < p rewrite <- H3 in H2.n, m, p:t
H:n < m -> m <= p -> n <= p
H1:n < m
H2:m < n
H3:n == p
n < p
      elim (lt_asymm n m); auto.
Qed.

Theorem le_trans : forall n m p, n <= m -> m <= p -> n <= p.forall n m p : t, n <= m -> m <= p -> n <= p
Proof.forall n m p : t, n <= m -> m <= p -> n <= p
intros n m p.n, m, p:t
n <= m -> m <= p -> n <= p rewrite 3 lt_eq_cases.n, m, p:t
n < m \/ n == m -> m < p \/ m == p -> n < p \/ n == p
intros [LT|EQ] [LT'|EQ']; try rewrite EQ; try rewrite <- EQ';
 generalize (lt_trans n m p); auto with relations.
Qed.

Some type classes about order

Instance lt_strorder : StrictOrder lt.StrictOrder lt
Proof.StrictOrder lt split.Irreflexive lt
Transitive lt -Irreflexive lt exact lt_irrefl. -Transitive lt exact lt_trans. Qed.

Instance le_preorder : PreOrder le.PreOrder le
Proof.PreOrder le split.Reflexive le
Transitive le -Reflexive le exact le_refl. -Transitive le exact le_trans. Qed.

Instance le_partialorder : PartialOrder _ le.PartialOrder eq le
Proof.PartialOrder eq le
intros x y.x, y:t
pointwise_lifting iff Tnil (x == y)
  (relation_conjunction le (Basics.flip le) x y) compute.x, y:t
(x == y -> x <= y <= x) /\ (x <= y <= x -> x == y) split.x, y:t
x == y -> x <= y <= x
x, y:t
x <= y <= x -> x == y
-x, y:t
x == y -> x <= y <= x intro EQ; now rewrite EQ.
-x, y:t
x <= y <= x -> x == y rewrite 2 lt_eq_cases.x, y:t
(x < y \/ x == y) /\ (y < x \/ y == x) -> x == y intuition.x, y:t
H:x < y
H0:y < x
x == y elim (lt_irrefl x).x, y:t
H:x < y
H0:y < x
x < x now transitivity y.
Qed.

We know enough now to benefit from the generic order tactic.

Definition lt_compat := lt_wd.
Definition lt_total := lt_trichotomy.
Definition le_lteq := lt_eq_cases.

Module Private_OrderTac.
Module IsTotal.
 Definition eq_equiv := eq_equiv.
 Definition lt_strorder := lt_strorder.
 Definition lt_compat := lt_compat.
 Definition lt_total := lt_total.
 Definition le_lteq := le_lteq.
End IsTotal.
Module Tac := !MakeOrderTac NZ IsTotal.
End Private_OrderTac.
Ltac order := Private_OrderTac.Tac.order.

Some direct consequences of order.

Theorem lt_neq : forall n m, n < m -> n ~= m.forall n m : t, n < m -> n ~= m
Proof.forall n m : t, n < m -> n ~= m order. Qed.

Theorem le_neq : forall n m, n < m <-> n <= m /\ n ~= m.forall n m : t, n < m <-> n <= m /\ n ~= m
Proof.forall n m : t, n < m <-> n <= m /\ n ~= m intuition order. Qed.

Theorem eq_le_incl : forall n m, n == m -> n <= m.forall n m : t, n == m -> n <= m
Proof.forall n m : t, n == m -> n <= m order. Qed.

Lemma lt_stepl : forall x y z, x < y -> x == z -> z < y.forall x y z : t, x < y -> x == z -> z < y
Proof.forall x y z : t, x < y -> x == z -> z < y order. Qed.

Lemma lt_stepr : forall x y z, x < y -> y == z -> x < z.forall x y z : t, x < y -> y == z -> x < z
Proof.forall x y z : t, x < y -> y == z -> x < z order. Qed.

Lemma le_stepl : forall x y z, x <= y -> x == z -> z <= y.forall x y z : t, x <= y -> x == z -> z <= y
Proof.forall x y z : t, x <= y -> x == z -> z <= y order. Qed.

Lemma le_stepr : forall x y z, x <= y -> y == z -> x <= z.forall x y z : t, x <= y -> y == z -> x <= z
Proof.forall x y z : t, x <= y -> y == z -> x <= z order. Qed.

Declare Left  Step lt_stepl.
Declare Right Step lt_stepr.
Declare Left  Step le_stepl.
Declare Right Step le_stepr.

Theorem le_lt_trans : forall n m p, n <= m -> m < p -> n < p.forall n m p : t, n <= m -> m < p -> n < p
Proof.forall n m p : t, n <= m -> m < p -> n < p order. Qed.

Theorem lt_le_trans : forall n m p, n < m -> m <= p -> n < p.forall n m p : t, n < m -> m <= p -> n < p
Proof.forall n m p : t, n < m -> m <= p -> n < p order. Qed.

Theorem le_antisymm : forall n m, n <= m -> m <= n -> n == m.forall n m : t, n <= m -> m <= n -> n == m
Proof.forall n m : t, n <= m -> m <= n -> n == m order. Qed.

More properties of < and ≤ with respect to S and 0.

Theorem le_succ_r : forall n m, n <= S m <-> n <= m \/ n == S m.forall n m : t, n <= S m <-> n <= m \/ n == S m
Proof.forall n m : t, n <= S m <-> n <= m \/ n == S m
intros n m; rewrite lt_eq_cases.n, m:t
n < S m \/ n == S m <-> n <= m \/ n == S m now rewrite lt_succ_r.
Qed.

Theorem lt_succ_l : forall n m, S n < m -> n < m.forall n m : t, S n < m -> n < m
Proof.forall n m : t, S n < m -> n < m
intros n m H; apply le_succ_l; order.
Qed.

Theorem le_le_succ_r : forall n m, n <= m -> n <= S m.forall n m : t, n <= m -> n <= S m
Proof.forall n m : t, n <= m -> n <= S m
intros n m LE.n, m:t
LE:n <= m
n <= S m apply lt_succ_r in LE.n, m:t
LE:n < S m
n <= S m order.
Qed.

Theorem lt_lt_succ_r : forall n m, n < m -> n < S m.forall n m : t, n < m -> n < S m
Proof.forall n m : t, n < m -> n < S m
intros.n, m:t
H:n < m
n < S m rewrite lt_succ_r.n, m:t
H:n < m
n <= m order.
Qed.

Theorem succ_lt_mono : forall n m, n < m <-> S n < S m.forall n m : t, n < m <-> S n < S m
Proof.forall n m : t, n < m <-> S n < S m
intros n m.n, m:t
n < m <-> S n < S m rewrite <- le_succ_l.n, m:t
S n <= m <-> S n < S m symmetry.n, m:t
S n < S m <-> S n <= m apply lt_succ_r.
Qed.

Theorem succ_le_mono : forall n m, n <= m <-> S n <= S m.forall n m : t, n <= m <-> S n <= S m
Proof.forall n m : t, n <= m <-> S n <= S m
intros n m.n, m:t
n <= m <-> S n <= S m now rewrite 2 lt_eq_cases, <- succ_lt_mono, succ_inj_wd.
Qed.

Theorem lt_0_1 : 0 < 1.0 < 1
Proof.0 < 1
rewrite one_succ.0 < S 0 apply lt_succ_diag_r.
Qed.

Theorem le_0_1 : 0 <= 1.0 <= 1
Proof.0 <= 1
apply lt_le_incl, lt_0_1.
Qed.

Theorem lt_1_2 : 1 < 2.1 < 2
Proof.1 < 2
rewrite two_succ.1 < S 1 apply lt_succ_diag_r.
Qed.

Theorem lt_0_2 : 0 < 2.0 < 2
Proof.0 < 2
  transitivity 1.0 < 1
1 < 2 -0 < 1 apply lt_0_1. -1 < 2 apply lt_1_2.
Qed.

Theorem le_0_2 : 0 <= 2.0 <= 2
Proof.0 <= 2
apply lt_le_incl, lt_0_2.
Qed.

The order tactic enriched with some knowledge of 0,1,2

Ltac order' := generalize lt_0_1 lt_1_2; order.

Theorem lt_1_l : forall n m, 0 < n -> n < m -> 1 < m.forall n m : t, 0 < n -> n < m -> 1 < m
Proof.forall n m : t, 0 < n -> n < m -> 1 < m
intros n m H1 H2.n, m:t
H1:0 < n
H2:n < m
1 < m rewrite <- le_succ_l, <- one_succ in H1.n, m:t
H1:1 <= n
H2:n < m
1 < m order.
Qed.

More Trichotomy, decidability and double negation elimination.

The following theorem is cleary redundant, but helps not to remember whether one has to say le_gt_cases or lt_ge_cases

Theorem lt_ge_cases : forall n m, n < m \/ n >= m.forall n m : t, n < m \/ m <= n
Proof.forall n m : t, n < m \/ m <= n
intros n m; destruct (le_gt_cases m n); intuition order.
Qed.

Theorem le_ge_cases : forall n m, n <= m \/ n >= m.forall n m : t, n <= m \/ m <= n
Proof.forall n m : t, n <= m \/ m <= n
intros n m; destruct (le_gt_cases n m); intuition order.
Qed.

Theorem lt_gt_cases : forall n m, n ~= m <-> n < m \/ n > m.forall n m : t, n ~= m <-> n < m \/ m < n
Proof.forall n m : t, n ~= m <-> n < m \/ m < n
intros n m; destruct (lt_trichotomy n m); intuition order.
Qed.

Decidability of equality, even though true in each finite ring, does not have a uniform proof. Otherwise, the proof for two fixed numbers would reduce to a normal form that will say if the numbers are equal or not, which cannot be true in all finite rings. Therefore, we prove decidability in the presence of order.

Theorem eq_decidable : forall n m, decidable (n == m).forall n m : t, decidable (n == m)
Proof.forall n m : t, decidable (n == m)
intros n m; destruct (lt_trichotomy n m) as [ | [ | ]];
 (right; order) || (left; order).
Qed.

DNE stands for double-negation elimination

Theorem eq_dne : forall n m, ~ ~ n == m <-> n == m.forall n m : t, ~ n ~= m <-> n == m
Proof.forall n m : t, ~ n ~= m <-> n == m
intros n m; split; intro H.n, m:t
H:~ n ~= m
n == m
n, m:t
H:n == m
~ n ~= m
-n, m:t
H:~ n ~= m
n == m destruct (eq_decidable n m) as [H1 | H1].n, m:t
H:~ n ~= m
H1:n == m
n == m
n, m:t
H:~ n ~= m
H1:n ~= m
n == m
  +n, m:t
H:~ n ~= m
H1:n == m
n == m assumption. +n, m:t
H:~ n ~= m
H1:n ~= m
n == m false_hyp H1 H.
-n, m:t
H:n == m
~ n ~= m intro H1; now apply H1.
Qed.

Theorem le_ngt : forall n m, n <= m <-> ~ n > m.forall n m : t, n <= m <-> ~ m < n
Proof.forall n m : t, n <= m <-> ~ m < n intuition order. Qed.

Redundant but useful

Theorem nlt_ge : forall n m, ~ n < m <-> n >= m.forall n m : t, ~ n < m <-> m <= n
Proof.forall n m : t, ~ n < m <-> m <= n intuition order. Qed.

Theorem lt_decidable : forall n m, decidable (n < m).forall n m : t, decidable (n < m)
Proof.forall n m : t, decidable (n < m)
intros n m; destruct (le_gt_cases m n); [right|left]; order.
Qed.

Theorem lt_dne : forall n m, ~ ~ n < m <-> n < m.forall n m : t, ~ ~ n < m <-> n < m
Proof.forall n m : t, ~ ~ n < m <-> n < m
intros n m; split; intro H.n, m:t
H:~ ~ n < m
n < m
n, m:t
H:n < m
~ ~ n < m
-n, m:t
H:~ ~ n < m
n < m destruct (lt_decidable n m) as [H1 | H1]; [assumption | false_hyp H1 H].
-n, m:t
H:n < m
~ ~ n < m intro H1; false_hyp H H1.
Qed.

Theorem nle_gt : forall n m, ~ n <= m <-> n > m.forall n m : t, ~ n <= m <-> m < n
Proof.forall n m : t, ~ n <= m <-> m < n intuition order. Qed.

Redundant but useful

Theorem lt_nge : forall n m, n < m <-> ~ n >= m.forall n m : t, n < m <-> ~ m <= n
Proof.forall n m : t, n < m <-> ~ m <= n intuition order. Qed.

Theorem le_decidable : forall n m, decidable (n <= m).forall n m : t, decidable (n <= m)
Proof.forall n m : t, decidable (n <= m)
intros n m; destruct (le_gt_cases n m); [left|right]; order.
Qed.

Theorem le_dne : forall n m, ~ ~ n <= m <-> n <= m.forall n m : t, ~ ~ n <= m <-> n <= m
Proof.forall n m : t, ~ ~ n <= m <-> n <= m
intros n m; split; intro H.n, m:t
H:~ ~ n <= m
n <= m
n, m:t
H:n <= m
~ ~ n <= m
-n, m:t
H:~ ~ n <= m
n <= m destruct (le_decidable n m) as [H1 | H1]; [assumption | false_hyp H1 H].
-n, m:t
H:n <= m
~ ~ n <= m intro H1; false_hyp H H1.
Qed.

Theorem nlt_succ_r : forall n m, ~ m < S n <-> n < m.forall n m : t, ~ m < S n <-> n < m
Proof.forall n m : t, ~ m < S n <-> n < m
intros n m; rewrite lt_succ_r.n, m:t
~ m <= n <-> n < m intuition order.
Qed.

The difference between integers and natural numbers is that for every integer there is a predecessor, which is not true for natural numbers. However, for both classes, every number that is bigger than some other number has a predecessor. The proof of this fact by regular induction does not go through, so we need to use strong (course-of-value) induction.

Lemma lt_exists_pred_strong :
  forall z n m, z < m -> m <= n -> exists k, m == S k /\ z <= k.forall z n m : t,
z < m -> m <= n -> exists k : t, m == S k /\ z <= k
Proof.forall z n m : t,
z < m -> m <= n -> exists k : t, m == S k /\ z <= k
intro z; nzinduct n z.z:t
forall m : t,
z < m -> m <= z -> exists k : t, m == S k /\ z <= k
z:t
forall n : t,
(forall m : t,
 z < m -> m <= n -> exists k : t, m == S k /\ z <= k) <->
(forall m : t,
 z < m -> m <= S n -> exists k : t, m == S k /\ z <= k)
-z:t
forall m : t,
z < m -> m <= z -> exists k : t, m == S k /\ z <= k order.
-z:t
forall n : t,
(forall m : t,
 z < m -> m <= n -> exists k : t, m == S k /\ z <= k) <->
(forall m : t,
 z < m -> m <= S n -> exists k : t, m == S k /\ z <= k) intro n; split; intros IH m H1 H2.z, n:t
IH:forall m0 : t,
z < m0 ->
m0 <= n -> exists k : t, m0 == S k /\ z <= k
m:t
H1:z < m
H2:m <= S n
exists k : t, m == S k /\ z <= k
z, n:t
IH:forall m0 : t,
z < m0 ->
m0 <= S n -> exists k : t, m0 == S k /\ z <= k
m:t
H1:z < m
H2:m <= n
exists k : t, m == S k /\ z <= k
  +z, n:t
IH:forall m0 : t,
z < m0 ->
m0 <= n -> exists k : t, m0 == S k /\ z <= k
m:t
H1:z < m
H2:m <= S n
exists k : t, m == S k /\ z <= k apply le_succ_r in H2.z, n:t
IH:forall m0 : t,
z < m0 ->
m0 <= n -> exists k : t, m0 == S k /\ z <= k
m:t
H1:z < m
H2:m <= n \/ m == S n
exists k : t, m == S k /\ z <= k destruct H2 as [H2 | H2].z, n:t
IH:forall m0 : t,
z < m0 ->
m0 <= n -> exists k : t, m0 == S k /\ z <= k
m:t
H1:z < m
H2:m <= n
exists k : t, m == S k /\ z <= k
z, n:t
IH:forall m0 : t,
z < m0 ->
m0 <= n -> exists k : t, m0 == S k /\ z <= k
m:t
H1:z < m
H2:m == S n
exists k : t, m == S k /\ z <= k
    *z, n:t
IH:forall m0 : t,
z < m0 ->
m0 <= n -> exists k : t, m0 == S k /\ z <= k
m:t
H1:z < m
H2:m <= n
exists k : t, m == S k /\ z <= k now apply IH. *z, n:t
IH:forall m0 : t,
z < m0 ->
m0 <= n -> exists k : t, m0 == S k /\ z <= k
m:t
H1:z < m
H2:m == S n
exists k : t, m == S k /\ z <= k exists n.z, n:t
IH:forall m0 : t,
z < m0 ->
m0 <= n -> exists k : t, m0 == S k /\ z <= k
m:t
H1:z < m
H2:m == S n
m == S n /\ z <= n now split; [| rewrite <- lt_succ_r; rewrite <- H2].
  +z, n:t
IH:forall m0 : t,
z < m0 ->
m0 <= S n -> exists k : t, m0 == S k /\ z <= k
m:t
H1:z < m
H2:m <= n
exists k : t, m == S k /\ z <= k apply IH.z, n:t
IH:forall m0 : t,
z < m0 ->
m0 <= S n -> exists k : t, m0 == S k /\ z <= k
m:t
H1:z < m
H2:m <= n
z < m
z, n:t
IH:forall m0 : t,
z < m0 ->
m0 <= S n -> exists k : t, m0 == S k /\ z <= k
m:t
H1:z < m
H2:m <= n
m <= S n *z, n:t
IH:forall m0 : t,
z < m0 ->
m0 <= S n -> exists k : t, m0 == S k /\ z <= k
m:t
H1:z < m
H2:m <= n
z < m assumption. *z, n:t
IH:forall m0 : t,
z < m0 ->
m0 <= S n -> exists k : t, m0 == S k /\ z <= k
m:t
H1:z < m
H2:m <= n
m <= S n now apply le_le_succ_r.
Qed.

Theorem lt_exists_pred :
  forall z n, z < n -> exists k, n == S k /\ z <= k.forall z n : t,
z < n -> exists k : t, n == S k /\ z <= k
Proof.forall z n : t,
z < n -> exists k : t, n == S k /\ z <= k
intros z n H; apply lt_exists_pred_strong with (z := z) (n := n).z, n:t
H:z < n
z < n
z, n:t
H:z < n
n <= n
-z, n:t
H:z < n
z < n assumption. -z, n:t
H:z < n
n <= n apply le_refl.
Qed.

Lemma lt_succ_pred : forall z n, z < n -> S (P n) == n.forall z n : t, z < n -> S (P n) == n
Proof.forall z n : t, z < n -> S (P n) == n
 intros z n H.z, n:t
H:z < n
S (P n) == n
 destruct (lt_exists_pred _ _ H) as (n' & EQ & LE).z, n:t
H:z < n
n':t
EQ:n == S n'
LE:z <= n'
S (P n) == n
 rewrite EQ.z, n:t
H:z < n
n':t
EQ:n == S n'
LE:z <= n'
S (P (S n')) == S n' now rewrite pred_succ.
Qed.

Stronger variant of induction with assumptions n >= 0 (n < 0) in the induction step

Section Induction.

Variable A : t -> Prop.
Hypothesis A_wd : Proper (eq==>iff) A.

Section Center.

Variable z : t. (* A z is the basis of induction *)

Section RightInduction.

Let A' (n : t) := forall m, z <= m -> m < n -> A m.
Let right_step :=   forall n, z <= n -> A n -> A (S n).
Let right_step' :=  forall n, z <= n -> A' n -> A n.
Let right_step'' := forall n, A' n <-> A' (S n).

Lemma rs_rs' :  A z -> right_step -> right_step'.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n : t => forall m : t, z <= m -> m < n -> A m:t -> Prop
right_step:=forall n : t, z <= n -> A n -> A (S n):Prop
right_step':=forall n : t, z <= n -> A' n -> A n:Prop
right_step'':=forall n : t, A' n <-> A' (S n):Prop
A z -> right_step -> right_step'
Proof.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n : t => forall m : t, z <= m -> m < n -> A m:t -> Prop
right_step:=forall n : t, z <= n -> A n -> A (S n):Prop
right_step':=forall n : t, z <= n -> A' n -> A n:Prop
right_step'':=forall n : t, A' n <-> A' (S n):Prop
A z -> right_step -> right_step'
intros Az RS n H1 H2.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, z <= m -> m < n0 -> A m:t -> Prop
right_step:=forall n0 : t, z <= n0 -> A n0 -> A (S n0):Prop
right_step':=forall n0 : t, z <= n0 -> A' n0 -> A n0:Prop
right_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
Az:A z
RS:right_step
n:t
H1:z <= n
H2:A' n
A n
le_elim H1.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, z <= m -> m < n0 -> A m:t -> Prop
right_step:=forall n0 : t, z <= n0 -> A n0 -> A (S n0):Prop
right_step':=forall n0 : t, z <= n0 -> A' n0 -> A n0:Prop
right_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
Az:A z
RS:right_step
n:t
H1:z < n
H2:A' n
A n
A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, z <= m -> m < n0 -> A m:t -> Prop
right_step:=forall n0 : t, z <= n0 -> A n0 -> A (S n0):Prop
right_step':=forall n0 : t, z <= n0 -> A' n0 -> A n0:Prop
right_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
Az:A z
RS:right_step
n:t
H1:z == n
H2:A' n
A n
-A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, z <= m -> m < n0 -> A m:t -> Prop
right_step:=forall n0 : t, z <= n0 -> A n0 -> A (S n0):Prop
right_step':=forall n0 : t, z <= n0 -> A' n0 -> A n0:Prop
right_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
Az:A z
RS:right_step
n:t
H1:z < n
H2:A' n
A n apply lt_exists_pred in H1.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, z <= m -> m < n0 -> A m:t -> Prop
right_step:=forall n0 : t, z <= n0 -> A n0 -> A (S n0):Prop
right_step':=forall n0 : t, z <= n0 -> A' n0 -> A n0:Prop
right_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
Az:A z
RS:right_step
n:t
H1:exists k : t, n == S k /\ z <= k
H2:A' n
A n destruct H1 as [k [H3 H4]].A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, z <= m -> m < n0 -> A m:t -> Prop
right_step:=forall n0 : t, z <= n0 -> A n0 -> A (S n0):Prop
right_step':=forall n0 : t, z <= n0 -> A' n0 -> A n0:Prop
right_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
Az:A z
RS:right_step
n, k:t
H3:n == S k
H4:z <= k
H2:A' n
A n
  rewrite H3.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, z <= m -> m < n0 -> A m:t -> Prop
right_step:=forall n0 : t, z <= n0 -> A n0 -> A (S n0):Prop
right_step':=forall n0 : t, z <= n0 -> A' n0 -> A n0:Prop
right_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
Az:A z
RS:right_step
n, k:t
H3:n == S k
H4:z <= k
H2:A' n
A (S k) apply RS; trivial.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, z <= m -> m < n0 -> A m:t -> Prop
right_step:=forall n0 : t, z <= n0 -> A n0 -> A (S n0):Prop
right_step':=forall n0 : t, z <= n0 -> A' n0 -> A n0:Prop
right_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
Az:A z
RS:right_step
n, k:t
H3:n == S k
H4:z <= k
H2:A' n
A k apply H2; trivial.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, z <= m -> m < n0 -> A m:t -> Prop
right_step:=forall n0 : t, z <= n0 -> A n0 -> A (S n0):Prop
right_step':=forall n0 : t, z <= n0 -> A' n0 -> A n0:Prop
right_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
Az:A z
RS:right_step
n, k:t
H3:n == S k
H4:z <= k
H2:A' n
k < n
  rewrite H3; apply lt_succ_diag_r.
-A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, z <= m -> m < n0 -> A m:t -> Prop
right_step:=forall n0 : t, z <= n0 -> A n0 -> A (S n0):Prop
right_step':=forall n0 : t, z <= n0 -> A' n0 -> A n0:Prop
right_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
Az:A z
RS:right_step
n:t
H1:z == n
H2:A' n
A n rewrite <- H1; apply Az.
Qed.

Lemma rs'_rs'' : right_step' -> right_step''.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n : t => forall m : t, z <= m -> m < n -> A m:t -> Prop
right_step:=forall n : t, z <= n -> A n -> A (S n):Prop
right_step':=forall n : t, z <= n -> A' n -> A n:Prop
right_step'':=forall n : t, A' n <-> A' (S n):Prop
right_step' -> right_step''
Proof.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n : t => forall m : t, z <= m -> m < n -> A m:t -> Prop
right_step:=forall n : t, z <= n -> A n -> A (S n):Prop
right_step':=forall n : t, z <= n -> A' n -> A n:Prop
right_step'':=forall n : t, A' n <-> A' (S n):Prop
right_step' -> right_step''
intros RS' n; split; intros H1 m H2 H3.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m0 : t, z <= m0 -> m0 < n0 -> A m0:t -> Prop
right_step:=forall n0 : t, z <= n0 -> A n0 -> A (S n0):Prop
right_step':=forall n0 : t, z <= n0 -> A' n0 -> A n0:Prop
right_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
RS':right_step'
n:t
H1:A' n
m:t
H2:z <= m
H3:m < S n
A m
A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m0 : t, z <= m0 -> m0 < n0 -> A m0:t -> Prop
right_step:=forall n0 : t, z <= n0 -> A n0 -> A (S n0):Prop
right_step':=forall n0 : t, z <= n0 -> A' n0 -> A n0:Prop
right_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
RS':right_step'
n:t
H1:A' (S n)
m:t
H2:z <= m
H3:m < n
A m
-A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m0 : t, z <= m0 -> m0 < n0 -> A m0:t -> Prop
right_step:=forall n0 : t, z <= n0 -> A n0 -> A (S n0):Prop
right_step':=forall n0 : t, z <= n0 -> A' n0 -> A n0:Prop
right_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
RS':right_step'
n:t
H1:A' n
m:t
H2:z <= m
H3:m < S n
A m apply lt_succ_r in H3; le_elim H3;
    [now apply H1 | rewrite H3 in *; now apply RS'].
-A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m0 : t, z <= m0 -> m0 < n0 -> A m0:t -> Prop
right_step:=forall n0 : t, z <= n0 -> A n0 -> A (S n0):Prop
right_step':=forall n0 : t, z <= n0 -> A' n0 -> A n0:Prop
right_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
RS':right_step'
n:t
H1:A' (S n)
m:t
H2:z <= m
H3:m < n
A m apply H1; [assumption | now apply lt_lt_succ_r].
Qed.

Lemma rbase : A' z.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n : t => forall m : t, z <= m -> m < n -> A m:t -> Prop
right_step:=forall n : t, z <= n -> A n -> A (S n):Prop
right_step':=forall n : t, z <= n -> A' n -> A n:Prop
right_step'':=forall n : t, A' n <-> A' (S n):Prop
A' z
Proof.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n : t => forall m : t, z <= m -> m < n -> A m:t -> Prop
right_step:=forall n : t, z <= n -> A n -> A (S n):Prop
right_step':=forall n : t, z <= n -> A' n -> A n:Prop
right_step'':=forall n : t, A' n <-> A' (S n):Prop
A' z
intros m H1 H2.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n : t =>
forall m0 : t, z <= m0 -> m0 < n -> A m0:t -> Prop
right_step:=forall n : t, z <= n -> A n -> A (S n):Prop
right_step':=forall n : t, z <= n -> A' n -> A n:Prop
right_step'':=forall n : t, A' n <-> A' (S n):Prop
m:t
H1:z <= m
H2:m < z
A m apply le_ngt in H1.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n : t =>
forall m0 : t, z <= m0 -> m0 < n -> A m0:t -> Prop
right_step:=forall n : t, z <= n -> A n -> A (S n):Prop
right_step':=forall n : t, z <= n -> A' n -> A n:Prop
right_step'':=forall n : t, A' n <-> A' (S n):Prop
m:t
H1:~ m < z
H2:m < z
A m false_hyp H2 H1.
Qed.

Lemma A'A_right : (forall n, A' n) -> forall n, z <= n -> A n.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n : t => forall m : t, z <= m -> m < n -> A m:t -> Prop
right_step:=forall n : t, z <= n -> A n -> A (S n):Prop
right_step':=forall n : t, z <= n -> A' n -> A n:Prop
right_step'':=forall n : t, A' n <-> A' (S n):Prop
(forall n : t, A' n) -> forall n : t, z <= n -> A n
Proof.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n : t => forall m : t, z <= m -> m < n -> A m:t -> Prop
right_step:=forall n : t, z <= n -> A n -> A (S n):Prop
right_step':=forall n : t, z <= n -> A' n -> A n:Prop
right_step'':=forall n : t, A' n <-> A' (S n):Prop
(forall n : t, A' n) -> forall n : t, z <= n -> A n
intros H1 n H2.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, z <= m -> m < n0 -> A m:t -> Prop
right_step:=forall n0 : t, z <= n0 -> A n0 -> A (S n0):Prop
right_step':=forall n0 : t, z <= n0 -> A' n0 -> A n0:Prop
right_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
H1:forall n0 : t, A' n0
n:t
H2:z <= n
A n apply H1 with (n := S n); [assumption | apply lt_succ_diag_r].
Qed.

Theorem strong_right_induction: right_step' -> forall n, z <= n -> A n.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n : t => forall m : t, z <= m -> m < n -> A m:t -> Prop
right_step:=forall n : t, z <= n -> A n -> A (S n):Prop
right_step':=forall n : t, z <= n -> A' n -> A n:Prop
right_step'':=forall n : t, A' n <-> A' (S n):Prop
right_step' -> forall n : t, z <= n -> A n
Proof.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n : t => forall m : t, z <= m -> m < n -> A m:t -> Prop
right_step:=forall n : t, z <= n -> A n -> A (S n):Prop
right_step':=forall n : t, z <= n -> A' n -> A n:Prop
right_step'':=forall n : t, A' n <-> A' (S n):Prop
right_step' -> forall n : t, z <= n -> A n
intro RS'; apply A'A_right; unfold A'; nzinduct n z;
[apply rbase | apply rs'_rs''; apply RS'].
Qed.

Theorem right_induction : A z -> right_step -> forall n, z <= n -> A n.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n : t => forall m : t, z <= m -> m < n -> A m:t -> Prop
right_step:=forall n : t, z <= n -> A n -> A (S n):Prop
right_step':=forall n : t, z <= n -> A' n -> A n:Prop
right_step'':=forall n : t, A' n <-> A' (S n):Prop
A z -> right_step -> forall n : t, z <= n -> A n
Proof.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n : t => forall m : t, z <= m -> m < n -> A m:t -> Prop
right_step:=forall n : t, z <= n -> A n -> A (S n):Prop
right_step':=forall n : t, z <= n -> A' n -> A n:Prop
right_step'':=forall n : t, A' n <-> A' (S n):Prop
A z -> right_step -> forall n : t, z <= n -> A n
intros Az RS; apply strong_right_induction; now apply rs_rs'.
Qed.

Theorem right_induction' :
  (forall n, n <= z -> A n) -> right_step -> forall n, A n.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n : t => forall m : t, z <= m -> m < n -> A m:t -> Prop
right_step:=forall n : t, z <= n -> A n -> A (S n):Prop
right_step':=forall n : t, z <= n -> A' n -> A n:Prop
right_step'':=forall n : t, A' n <-> A' (S n):Prop
(forall n : t, n <= z -> A n) ->
right_step -> forall n : t, A n
Proof.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n : t => forall m : t, z <= m -> m < n -> A m:t -> Prop
right_step:=forall n : t, z <= n -> A n -> A (S n):Prop
right_step':=forall n : t, z <= n -> A' n -> A n:Prop
right_step'':=forall n : t, A' n <-> A' (S n):Prop
(forall n : t, n <= z -> A n) ->
right_step -> forall n : t, A n
intros L R n.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, z <= m -> m < n0 -> A m:t -> Prop
right_step:=forall n0 : t, z <= n0 -> A n0 -> A (S n0):Prop
right_step':=forall n0 : t, z <= n0 -> A' n0 -> A n0:Prop
right_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
L:forall n0 : t, n0 <= z -> A n0
R:right_step
n:t
A n
destruct (lt_trichotomy n z) as [H | [H | H]].A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, z <= m -> m < n0 -> A m:t -> Prop
right_step:=forall n0 : t, z <= n0 -> A n0 -> A (S n0):Prop
right_step':=forall n0 : t, z <= n0 -> A' n0 -> A n0:Prop
right_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
L:forall n0 : t, n0 <= z -> A n0
R:right_step
n:t
H:n < z
A n
A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, z <= m -> m < n0 -> A m:t -> Prop
right_step:=forall n0 : t, z <= n0 -> A n0 -> A (S n0):Prop
right_step':=forall n0 : t, z <= n0 -> A' n0 -> A n0:Prop
right_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
L:forall n0 : t, n0 <= z -> A n0
R:right_step
n:t
H:n == z
A n
A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, z <= m -> m < n0 -> A m:t -> Prop
right_step:=forall n0 : t, z <= n0 -> A n0 -> A (S n0):Prop
right_step':=forall n0 : t, z <= n0 -> A' n0 -> A n0:Prop
right_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
L:forall n0 : t, n0 <= z -> A n0
R:right_step
n:t
H:z < n
A n
-A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, z <= m -> m < n0 -> A m:t -> Prop
right_step:=forall n0 : t, z <= n0 -> A n0 -> A (S n0):Prop
right_step':=forall n0 : t, z <= n0 -> A' n0 -> A n0:Prop
right_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
L:forall n0 : t, n0 <= z -> A n0
R:right_step
n:t
H:n < z
A n apply L; now apply lt_le_incl.
-A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, z <= m -> m < n0 -> A m:t -> Prop
right_step:=forall n0 : t, z <= n0 -> A n0 -> A (S n0):Prop
right_step':=forall n0 : t, z <= n0 -> A' n0 -> A n0:Prop
right_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
L:forall n0 : t, n0 <= z -> A n0
R:right_step
n:t
H:n == z
A n apply L; now apply eq_le_incl.
-A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, z <= m -> m < n0 -> A m:t -> Prop
right_step:=forall n0 : t, z <= n0 -> A n0 -> A (S n0):Prop
right_step':=forall n0 : t, z <= n0 -> A' n0 -> A n0:Prop
right_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
L:forall n0 : t, n0 <= z -> A n0
R:right_step
n:t
H:z < n
A n apply right_induction.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, z <= m -> m < n0 -> A m:t -> Prop
right_step:=forall n0 : t, z <= n0 -> A n0 -> A (S n0):Prop
right_step':=forall n0 : t, z <= n0 -> A' n0 -> A n0:Prop
right_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
L:forall n0 : t, n0 <= z -> A n0
R:right_step
n:t
H:z < n
A z
A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, z <= m -> m < n0 -> A m:t -> Prop
right_step:=forall n0 : t, z <= n0 -> A n0 -> A (S n0):Prop
right_step':=forall n0 : t, z <= n0 -> A' n0 -> A n0:Prop
right_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
L:forall n0 : t, n0 <= z -> A n0
R:right_step
n:t
H:z < n
right_step
A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, z <= m -> m < n0 -> A m:t -> Prop
right_step:=forall n0 : t, z <= n0 -> A n0 -> A (S n0):Prop
right_step':=forall n0 : t, z <= n0 -> A' n0 -> A n0:Prop
right_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
L:forall n0 : t, n0 <= z -> A n0
R:right_step
n:t
H:z < n
z <= n
  +A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, z <= m -> m < n0 -> A m:t -> Prop
right_step:=forall n0 : t, z <= n0 -> A n0 -> A (S n0):Prop
right_step':=forall n0 : t, z <= n0 -> A' n0 -> A n0:Prop
right_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
L:forall n0 : t, n0 <= z -> A n0
R:right_step
n:t
H:z < n
A z apply L; now apply eq_le_incl.
  +A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, z <= m -> m < n0 -> A m:t -> Prop
right_step:=forall n0 : t, z <= n0 -> A n0 -> A (S n0):Prop
right_step':=forall n0 : t, z <= n0 -> A' n0 -> A n0:Prop
right_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
L:forall n0 : t, n0 <= z -> A n0
R:right_step
n:t
H:z < n
right_step assumption.
  +A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, z <= m -> m < n0 -> A m:t -> Prop
right_step:=forall n0 : t, z <= n0 -> A n0 -> A (S n0):Prop
right_step':=forall n0 : t, z <= n0 -> A' n0 -> A n0:Prop
right_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
L:forall n0 : t, n0 <= z -> A n0
R:right_step
n:t
H:z < n
z <= n now apply lt_le_incl.
Qed.

Theorem strong_right_induction' :
  (forall n, n <= z -> A n) -> right_step' -> forall n, A n.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n : t => forall m : t, z <= m -> m < n -> A m:t -> Prop
right_step:=forall n : t, z <= n -> A n -> A (S n):Prop
right_step':=forall n : t, z <= n -> A' n -> A n:Prop
right_step'':=forall n : t, A' n <-> A' (S n):Prop
(forall n : t, n <= z -> A n) ->
right_step' -> forall n : t, A n
Proof.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n : t => forall m : t, z <= m -> m < n -> A m:t -> Prop
right_step:=forall n : t, z <= n -> A n -> A (S n):Prop
right_step':=forall n : t, z <= n -> A' n -> A n:Prop
right_step'':=forall n : t, A' n <-> A' (S n):Prop
(forall n : t, n <= z -> A n) ->
right_step' -> forall n : t, A n
intros L R n.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, z <= m -> m < n0 -> A m:t -> Prop
right_step:=forall n0 : t, z <= n0 -> A n0 -> A (S n0):Prop
right_step':=forall n0 : t, z <= n0 -> A' n0 -> A n0:Prop
right_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
L:forall n0 : t, n0 <= z -> A n0
R:right_step'
n:t
A n
destruct (lt_trichotomy n z) as [H | [H | H]].A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, z <= m -> m < n0 -> A m:t -> Prop
right_step:=forall n0 : t, z <= n0 -> A n0 -> A (S n0):Prop
right_step':=forall n0 : t, z <= n0 -> A' n0 -> A n0:Prop
right_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
L:forall n0 : t, n0 <= z -> A n0
R:right_step'
n:t
H:n < z
A n
A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, z <= m -> m < n0 -> A m:t -> Prop
right_step:=forall n0 : t, z <= n0 -> A n0 -> A (S n0):Prop
right_step':=forall n0 : t, z <= n0 -> A' n0 -> A n0:Prop
right_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
L:forall n0 : t, n0 <= z -> A n0
R:right_step'
n:t
H:n == z
A n
A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, z <= m -> m < n0 -> A m:t -> Prop
right_step:=forall n0 : t, z <= n0 -> A n0 -> A (S n0):Prop
right_step':=forall n0 : t, z <= n0 -> A' n0 -> A n0:Prop
right_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
L:forall n0 : t, n0 <= z -> A n0
R:right_step'
n:t
H:z < n
A n
-A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, z <= m -> m < n0 -> A m:t -> Prop
right_step:=forall n0 : t, z <= n0 -> A n0 -> A (S n0):Prop
right_step':=forall n0 : t, z <= n0 -> A' n0 -> A n0:Prop
right_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
L:forall n0 : t, n0 <= z -> A n0
R:right_step'
n:t
H:n < z
A n apply L; now apply lt_le_incl.
-A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, z <= m -> m < n0 -> A m:t -> Prop
right_step:=forall n0 : t, z <= n0 -> A n0 -> A (S n0):Prop
right_step':=forall n0 : t, z <= n0 -> A' n0 -> A n0:Prop
right_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
L:forall n0 : t, n0 <= z -> A n0
R:right_step'
n:t
H:n == z
A n apply L; now apply eq_le_incl.
-A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, z <= m -> m < n0 -> A m:t -> Prop
right_step:=forall n0 : t, z <= n0 -> A n0 -> A (S n0):Prop
right_step':=forall n0 : t, z <= n0 -> A' n0 -> A n0:Prop
right_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
L:forall n0 : t, n0 <= z -> A n0
R:right_step'
n:t
H:z < n
A n apply strong_right_induction.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, z <= m -> m < n0 -> A m:t -> Prop
right_step:=forall n0 : t, z <= n0 -> A n0 -> A (S n0):Prop
right_step':=forall n0 : t, z <= n0 -> A' n0 -> A n0:Prop
right_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
L:forall n0 : t, n0 <= z -> A n0
R:right_step'
n:t
H:z < n
right_step'
A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, z <= m -> m < n0 -> A m:t -> Prop
right_step:=forall n0 : t, z <= n0 -> A n0 -> A (S n0):Prop
right_step':=forall n0 : t, z <= n0 -> A' n0 -> A n0:Prop
right_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
L:forall n0 : t, n0 <= z -> A n0
R:right_step'
n:t
H:z < n
z <= n
  +A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, z <= m -> m < n0 -> A m:t -> Prop
right_step:=forall n0 : t, z <= n0 -> A n0 -> A (S n0):Prop
right_step':=forall n0 : t, z <= n0 -> A' n0 -> A n0:Prop
right_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
L:forall n0 : t, n0 <= z -> A n0
R:right_step'
n:t
H:z < n
right_step' assumption. +A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, z <= m -> m < n0 -> A m:t -> Prop
right_step:=forall n0 : t, z <= n0 -> A n0 -> A (S n0):Prop
right_step':=forall n0 : t, z <= n0 -> A' n0 -> A n0:Prop
right_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
L:forall n0 : t, n0 <= z -> A n0
R:right_step'
n:t
H:z < n
z <= n now apply lt_le_incl.
Qed.

End RightInduction.

Section LeftInduction.

Let A' (n : t) := forall m, m <= z -> n <= m -> A m.
Let left_step :=   forall n, n < z -> A (S n) -> A n.
Let left_step' :=  forall n, n <= z -> A' (S n) -> A n.
Let left_step'' := forall n, A' n <-> A' (S n).

Lemma ls_ls' :  A z -> left_step -> left_step'.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n : t => forall m : t, m <= z -> n <= m -> A m:t -> Prop
left_step:=forall n : t, n < z -> A (S n) -> A n:Prop
left_step':=forall n : t, n <= z -> A' (S n) -> A n:Prop
left_step'':=forall n : t, A' n <-> A' (S n):Prop
A z -> left_step -> left_step'
Proof.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n : t => forall m : t, m <= z -> n <= m -> A m:t -> Prop
left_step:=forall n : t, n < z -> A (S n) -> A n:Prop
left_step':=forall n : t, n <= z -> A' (S n) -> A n:Prop
left_step'':=forall n : t, A' n <-> A' (S n):Prop
A z -> left_step -> left_step'
intros Az LS n H1 H2.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, m <= z -> n0 <= m -> A m:t -> Prop
left_step:=forall n0 : t, n0 < z -> A (S n0) -> A n0:Prop
left_step':=forall n0 : t,
n0 <= z -> A' (S n0) -> A n0:Prop
left_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
Az:A z
LS:left_step
n:t
H1:n <= z
H2:A' (S n)
A n le_elim H1.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, m <= z -> n0 <= m -> A m:t -> Prop
left_step:=forall n0 : t, n0 < z -> A (S n0) -> A n0:Prop
left_step':=forall n0 : t,
n0 <= z -> A' (S n0) -> A n0:Prop
left_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
Az:A z
LS:left_step
n:t
H1:n < z
H2:A' (S n)
A n
A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, m <= z -> n0 <= m -> A m:t -> Prop
left_step:=forall n0 : t, n0 < z -> A (S n0) -> A n0:Prop
left_step':=forall n0 : t,
n0 <= z -> A' (S n0) -> A n0:Prop
left_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
Az:A z
LS:left_step
n:t
H1:n == z
H2:A' (S n)
A n
-A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, m <= z -> n0 <= m -> A m:t -> Prop
left_step:=forall n0 : t, n0 < z -> A (S n0) -> A n0:Prop
left_step':=forall n0 : t,
n0 <= z -> A' (S n0) -> A n0:Prop
left_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
Az:A z
LS:left_step
n:t
H1:n < z
H2:A' (S n)
A n apply LS; trivial.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, m <= z -> n0 <= m -> A m:t -> Prop
left_step:=forall n0 : t, n0 < z -> A (S n0) -> A n0:Prop
left_step':=forall n0 : t,
n0 <= z -> A' (S n0) -> A n0:Prop
left_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
Az:A z
LS:left_step
n:t
H1:n < z
H2:A' (S n)
A (S n) apply H2; [now apply le_succ_l | now apply eq_le_incl].
-A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, m <= z -> n0 <= m -> A m:t -> Prop
left_step:=forall n0 : t, n0 < z -> A (S n0) -> A n0:Prop
left_step':=forall n0 : t,
n0 <= z -> A' (S n0) -> A n0:Prop
left_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
Az:A z
LS:left_step
n:t
H1:n == z
H2:A' (S n)
A n rewrite H1; apply Az.
Qed.

Lemma ls'_ls'' : left_step' -> left_step''.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n : t => forall m : t, m <= z -> n <= m -> A m:t -> Prop
left_step:=forall n : t, n < z -> A (S n) -> A n:Prop
left_step':=forall n : t, n <= z -> A' (S n) -> A n:Prop
left_step'':=forall n : t, A' n <-> A' (S n):Prop
left_step' -> left_step''
Proof.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n : t => forall m : t, m <= z -> n <= m -> A m:t -> Prop
left_step:=forall n : t, n < z -> A (S n) -> A n:Prop
left_step':=forall n : t, n <= z -> A' (S n) -> A n:Prop
left_step'':=forall n : t, A' n <-> A' (S n):Prop
left_step' -> left_step''
intros LS' n; split; intros H1 m H2 H3.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m0 : t, m0 <= z -> n0 <= m0 -> A m0:t -> Prop
left_step:=forall n0 : t, n0 < z -> A (S n0) -> A n0:Prop
left_step':=forall n0 : t,
n0 <= z -> A' (S n0) -> A n0:Prop
left_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
LS':left_step'
n:t
H1:A' n
m:t
H2:m <= z
H3:S n <= m
A m
A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m0 : t, m0 <= z -> n0 <= m0 -> A m0:t -> Prop
left_step:=forall n0 : t, n0 < z -> A (S n0) -> A n0:Prop
left_step':=forall n0 : t,
n0 <= z -> A' (S n0) -> A n0:Prop
left_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
LS':left_step'
n:t
H1:A' (S n)
m:t
H2:m <= z
H3:n <= m
A m
-A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m0 : t, m0 <= z -> n0 <= m0 -> A m0:t -> Prop
left_step:=forall n0 : t, n0 < z -> A (S n0) -> A n0:Prop
left_step':=forall n0 : t,
n0 <= z -> A' (S n0) -> A n0:Prop
left_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
LS':left_step'
n:t
H1:A' n
m:t
H2:m <= z
H3:S n <= m
A m apply le_succ_l in H3.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m0 : t, m0 <= z -> n0 <= m0 -> A m0:t -> Prop
left_step:=forall n0 : t, n0 < z -> A (S n0) -> A n0:Prop
left_step':=forall n0 : t,
n0 <= z -> A' (S n0) -> A n0:Prop
left_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
LS':left_step'
n:t
H1:A' n
m:t
H2:m <= z
H3:n < m
A m apply lt_le_incl in H3.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m0 : t, m0 <= z -> n0 <= m0 -> A m0:t -> Prop
left_step:=forall n0 : t, n0 < z -> A (S n0) -> A n0:Prop
left_step':=forall n0 : t,
n0 <= z -> A' (S n0) -> A n0:Prop
left_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
LS':left_step'
n:t
H1:A' n
m:t
H2:m <= z
H3:n <= m
A m now apply H1.
-A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m0 : t, m0 <= z -> n0 <= m0 -> A m0:t -> Prop
left_step:=forall n0 : t, n0 < z -> A (S n0) -> A n0:Prop
left_step':=forall n0 : t,
n0 <= z -> A' (S n0) -> A n0:Prop
left_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
LS':left_step'
n:t
H1:A' (S n)
m:t
H2:m <= z
H3:n <= m
A m le_elim H3.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m0 : t, m0 <= z -> n0 <= m0 -> A m0:t -> Prop
left_step:=forall n0 : t, n0 < z -> A (S n0) -> A n0:Prop
left_step':=forall n0 : t,
n0 <= z -> A' (S n0) -> A n0:Prop
left_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
LS':left_step'
n:t
H1:A' (S n)
m:t
H2:m <= z
H3:n < m
A m
A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m0 : t, m0 <= z -> n0 <= m0 -> A m0:t -> Prop
left_step:=forall n0 : t, n0 < z -> A (S n0) -> A n0:Prop
left_step':=forall n0 : t,
n0 <= z -> A' (S n0) -> A n0:Prop
left_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
LS':left_step'
n:t
H1:A' (S n)
m:t
H2:m <= z
H3:n == m
A m
  +A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m0 : t, m0 <= z -> n0 <= m0 -> A m0:t -> Prop
left_step:=forall n0 : t, n0 < z -> A (S n0) -> A n0:Prop
left_step':=forall n0 : t,
n0 <= z -> A' (S n0) -> A n0:Prop
left_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
LS':left_step'
n:t
H1:A' (S n)
m:t
H2:m <= z
H3:n < m
A m apply le_succ_l in H3.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m0 : t, m0 <= z -> n0 <= m0 -> A m0:t -> Prop
left_step:=forall n0 : t, n0 < z -> A (S n0) -> A n0:Prop
left_step':=forall n0 : t,
n0 <= z -> A' (S n0) -> A n0:Prop
left_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
LS':left_step'
n:t
H1:A' (S n)
m:t
H2:m <= z
H3:S n <= m
A m now apply H1.
  +A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m0 : t, m0 <= z -> n0 <= m0 -> A m0:t -> Prop
left_step:=forall n0 : t, n0 < z -> A (S n0) -> A n0:Prop
left_step':=forall n0 : t,
n0 <= z -> A' (S n0) -> A n0:Prop
left_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
LS':left_step'
n:t
H1:A' (S n)
m:t
H2:m <= z
H3:n == m
A m rewrite <- H3 in *; now apply LS'.
Qed.

Lemma lbase : A' (S z).A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n : t => forall m : t, m <= z -> n <= m -> A m:t -> Prop
left_step:=forall n : t, n < z -> A (S n) -> A n:Prop
left_step':=forall n : t, n <= z -> A' (S n) -> A n:Prop
left_step'':=forall n : t, A' n <-> A' (S n):Prop
A' (S z)
Proof.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n : t => forall m : t, m <= z -> n <= m -> A m:t -> Prop
left_step:=forall n : t, n < z -> A (S n) -> A n:Prop
left_step':=forall n : t, n <= z -> A' (S n) -> A n:Prop
left_step'':=forall n : t, A' n <-> A' (S n):Prop
A' (S z)
intros m H1 H2.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n : t =>
forall m0 : t, m0 <= z -> n <= m0 -> A m0:t -> Prop
left_step:=forall n : t, n < z -> A (S n) -> A n:Prop
left_step':=forall n : t, n <= z -> A' (S n) -> A n:Prop
left_step'':=forall n : t, A' n <-> A' (S n):Prop
m:t
H1:m <= z
H2:S z <= m
A m apply le_succ_l in H2.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n : t =>
forall m0 : t, m0 <= z -> n <= m0 -> A m0:t -> Prop
left_step:=forall n : t, n < z -> A (S n) -> A n:Prop
left_step':=forall n : t, n <= z -> A' (S n) -> A n:Prop
left_step'':=forall n : t, A' n <-> A' (S n):Prop
m:t
H1:m <= z
H2:z < m
A m
apply le_ngt in H1.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n : t =>
forall m0 : t, m0 <= z -> n <= m0 -> A m0:t -> Prop
left_step:=forall n : t, n < z -> A (S n) -> A n:Prop
left_step':=forall n : t, n <= z -> A' (S n) -> A n:Prop
left_step'':=forall n : t, A' n <-> A' (S n):Prop
m:t
H1:~ z < m
H2:z < m
A m false_hyp H2 H1.
Qed.

Lemma A'A_left : (forall n, A' n) -> forall n, n <= z -> A n.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n : t => forall m : t, m <= z -> n <= m -> A m:t -> Prop
left_step:=forall n : t, n < z -> A (S n) -> A n:Prop
left_step':=forall n : t, n <= z -> A' (S n) -> A n:Prop
left_step'':=forall n : t, A' n <-> A' (S n):Prop
(forall n : t, A' n) -> forall n : t, n <= z -> A n
Proof.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n : t => forall m : t, m <= z -> n <= m -> A m:t -> Prop
left_step:=forall n : t, n < z -> A (S n) -> A n:Prop
left_step':=forall n : t, n <= z -> A' (S n) -> A n:Prop
left_step'':=forall n : t, A' n <-> A' (S n):Prop
(forall n : t, A' n) -> forall n : t, n <= z -> A n
intros H1 n H2.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, m <= z -> n0 <= m -> A m:t -> Prop
left_step:=forall n0 : t, n0 < z -> A (S n0) -> A n0:Prop
left_step':=forall n0 : t,
n0 <= z -> A' (S n0) -> A n0:Prop
left_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
H1:forall n0 : t, A' n0
n:t
H2:n <= z
A n apply (H1 n); [assumption | now apply eq_le_incl].
Qed.

Theorem strong_left_induction: left_step' -> forall n, n <= z -> A n.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n : t => forall m : t, m <= z -> n <= m -> A m:t -> Prop
left_step:=forall n : t, n < z -> A (S n) -> A n:Prop
left_step':=forall n : t, n <= z -> A' (S n) -> A n:Prop
left_step'':=forall n : t, A' n <-> A' (S n):Prop
left_step' -> forall n : t, n <= z -> A n
Proof.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n : t => forall m : t, m <= z -> n <= m -> A m:t -> Prop
left_step:=forall n : t, n < z -> A (S n) -> A n:Prop
left_step':=forall n : t, n <= z -> A' (S n) -> A n:Prop
left_step'':=forall n : t, A' n <-> A' (S n):Prop
left_step' -> forall n : t, n <= z -> A n
intro LS'; apply A'A_left; unfold A'; nzinduct n (S z);
[apply lbase | apply ls'_ls''; apply LS'].
Qed.

Theorem left_induction : A z -> left_step -> forall n, n <= z -> A n.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n : t => forall m : t, m <= z -> n <= m -> A m:t -> Prop
left_step:=forall n : t, n < z -> A (S n) -> A n:Prop
left_step':=forall n : t, n <= z -> A' (S n) -> A n:Prop
left_step'':=forall n : t, A' n <-> A' (S n):Prop
A z -> left_step -> forall n : t, n <= z -> A n
Proof.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n : t => forall m : t, m <= z -> n <= m -> A m:t -> Prop
left_step:=forall n : t, n < z -> A (S n) -> A n:Prop
left_step':=forall n : t, n <= z -> A' (S n) -> A n:Prop
left_step'':=forall n : t, A' n <-> A' (S n):Prop
A z -> left_step -> forall n : t, n <= z -> A n
intros Az LS; apply strong_left_induction; now apply ls_ls'.
Qed.

Theorem left_induction' :
  (forall n, z <= n -> A n) -> left_step -> forall n, A n.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n : t => forall m : t, m <= z -> n <= m -> A m:t -> Prop
left_step:=forall n : t, n < z -> A (S n) -> A n:Prop
left_step':=forall n : t, n <= z -> A' (S n) -> A n:Prop
left_step'':=forall n : t, A' n <-> A' (S n):Prop
(forall n : t, z <= n -> A n) ->
left_step -> forall n : t, A n
Proof.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n : t => forall m : t, m <= z -> n <= m -> A m:t -> Prop
left_step:=forall n : t, n < z -> A (S n) -> A n:Prop
left_step':=forall n : t, n <= z -> A' (S n) -> A n:Prop
left_step'':=forall n : t, A' n <-> A' (S n):Prop
(forall n : t, z <= n -> A n) ->
left_step -> forall n : t, A n
intros R L n.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, m <= z -> n0 <= m -> A m:t -> Prop
left_step:=forall n0 : t, n0 < z -> A (S n0) -> A n0:Prop
left_step':=forall n0 : t,
n0 <= z -> A' (S n0) -> A n0:Prop
left_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
R:forall n0 : t, z <= n0 -> A n0
L:left_step
n:t
A n
destruct (lt_trichotomy n z) as [H | [H | H]].A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, m <= z -> n0 <= m -> A m:t -> Prop
left_step:=forall n0 : t, n0 < z -> A (S n0) -> A n0:Prop
left_step':=forall n0 : t,
n0 <= z -> A' (S n0) -> A n0:Prop
left_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
R:forall n0 : t, z <= n0 -> A n0
L:left_step
n:t
H:n < z
A n
A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, m <= z -> n0 <= m -> A m:t -> Prop
left_step:=forall n0 : t, n0 < z -> A (S n0) -> A n0:Prop
left_step':=forall n0 : t,
n0 <= z -> A' (S n0) -> A n0:Prop
left_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
R:forall n0 : t, z <= n0 -> A n0
L:left_step
n:t
H:n == z
A n
A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, m <= z -> n0 <= m -> A m:t -> Prop
left_step:=forall n0 : t, n0 < z -> A (S n0) -> A n0:Prop
left_step':=forall n0 : t,
n0 <= z -> A' (S n0) -> A n0:Prop
left_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
R:forall n0 : t, z <= n0 -> A n0
L:left_step
n:t
H:z < n
A n
-A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, m <= z -> n0 <= m -> A m:t -> Prop
left_step:=forall n0 : t, n0 < z -> A (S n0) -> A n0:Prop
left_step':=forall n0 : t,
n0 <= z -> A' (S n0) -> A n0:Prop
left_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
R:forall n0 : t, z <= n0 -> A n0
L:left_step
n:t
H:n < z
A n apply left_induction.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, m <= z -> n0 <= m -> A m:t -> Prop
left_step:=forall n0 : t, n0 < z -> A (S n0) -> A n0:Prop
left_step':=forall n0 : t,
n0 <= z -> A' (S n0) -> A n0:Prop
left_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
R:forall n0 : t, z <= n0 -> A n0
L:left_step
n:t
H:n < z
A z
A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, m <= z -> n0 <= m -> A m:t -> Prop
left_step:=forall n0 : t, n0 < z -> A (S n0) -> A n0:Prop
left_step':=forall n0 : t,
n0 <= z -> A' (S n0) -> A n0:Prop
left_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
R:forall n0 : t, z <= n0 -> A n0
L:left_step
n:t
H:n < z
left_step
A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, m <= z -> n0 <= m -> A m:t -> Prop
left_step:=forall n0 : t, n0 < z -> A (S n0) -> A n0:Prop
left_step':=forall n0 : t,
n0 <= z -> A' (S n0) -> A n0:Prop
left_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
R:forall n0 : t, z <= n0 -> A n0
L:left_step
n:t
H:n < z
n <= z
  +A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, m <= z -> n0 <= m -> A m:t -> Prop
left_step:=forall n0 : t, n0 < z -> A (S n0) -> A n0:Prop
left_step':=forall n0 : t,
n0 <= z -> A' (S n0) -> A n0:Prop
left_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
R:forall n0 : t, z <= n0 -> A n0
L:left_step
n:t
H:n < z
A z apply R.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, m <= z -> n0 <= m -> A m:t -> Prop
left_step:=forall n0 : t, n0 < z -> A (S n0) -> A n0:Prop
left_step':=forall n0 : t,
n0 <= z -> A' (S n0) -> A n0:Prop
left_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
R:forall n0 : t, z <= n0 -> A n0
L:left_step
n:t
H:n < z
z <= z now apply eq_le_incl.
  +A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, m <= z -> n0 <= m -> A m:t -> Prop
left_step:=forall n0 : t, n0 < z -> A (S n0) -> A n0:Prop
left_step':=forall n0 : t,
n0 <= z -> A' (S n0) -> A n0:Prop
left_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
R:forall n0 : t, z <= n0 -> A n0
L:left_step
n:t
H:n < z
left_step assumption.
  +A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, m <= z -> n0 <= m -> A m:t -> Prop
left_step:=forall n0 : t, n0 < z -> A (S n0) -> A n0:Prop
left_step':=forall n0 : t,
n0 <= z -> A' (S n0) -> A n0:Prop
left_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
R:forall n0 : t, z <= n0 -> A n0
L:left_step
n:t
H:n < z
n <= z now apply lt_le_incl.
-A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, m <= z -> n0 <= m -> A m:t -> Prop
left_step:=forall n0 : t, n0 < z -> A (S n0) -> A n0:Prop
left_step':=forall n0 : t,
n0 <= z -> A' (S n0) -> A n0:Prop
left_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
R:forall n0 : t, z <= n0 -> A n0
L:left_step
n:t
H:n == z
A n rewrite H; apply R; now apply eq_le_incl.
-A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, m <= z -> n0 <= m -> A m:t -> Prop
left_step:=forall n0 : t, n0 < z -> A (S n0) -> A n0:Prop
left_step':=forall n0 : t,
n0 <= z -> A' (S n0) -> A n0:Prop
left_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
R:forall n0 : t, z <= n0 -> A n0
L:left_step
n:t
H:z < n
A n apply R; now apply lt_le_incl.
Qed.

Theorem strong_left_induction' :
  (forall n, z <= n -> A n) -> left_step' -> forall n, A n.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n : t => forall m : t, m <= z -> n <= m -> A m:t -> Prop
left_step:=forall n : t, n < z -> A (S n) -> A n:Prop
left_step':=forall n : t, n <= z -> A' (S n) -> A n:Prop
left_step'':=forall n : t, A' n <-> A' (S n):Prop
(forall n : t, z <= n -> A n) ->
left_step' -> forall n : t, A n
Proof.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n : t => forall m : t, m <= z -> n <= m -> A m:t -> Prop
left_step:=forall n : t, n < z -> A (S n) -> A n:Prop
left_step':=forall n : t, n <= z -> A' (S n) -> A n:Prop
left_step'':=forall n : t, A' n <-> A' (S n):Prop
(forall n : t, z <= n -> A n) ->
left_step' -> forall n : t, A n
intros R L n.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, m <= z -> n0 <= m -> A m:t -> Prop
left_step:=forall n0 : t, n0 < z -> A (S n0) -> A n0:Prop
left_step':=forall n0 : t,
n0 <= z -> A' (S n0) -> A n0:Prop
left_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
R:forall n0 : t, z <= n0 -> A n0
L:left_step'
n:t
A n
destruct (lt_trichotomy n z) as [H | [H | H]].A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, m <= z -> n0 <= m -> A m:t -> Prop
left_step:=forall n0 : t, n0 < z -> A (S n0) -> A n0:Prop
left_step':=forall n0 : t,
n0 <= z -> A' (S n0) -> A n0:Prop
left_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
R:forall n0 : t, z <= n0 -> A n0
L:left_step'
n:t
H:n < z
A n
A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, m <= z -> n0 <= m -> A m:t -> Prop
left_step:=forall n0 : t, n0 < z -> A (S n0) -> A n0:Prop
left_step':=forall n0 : t,
n0 <= z -> A' (S n0) -> A n0:Prop
left_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
R:forall n0 : t, z <= n0 -> A n0
L:left_step'
n:t
H:n == z
A n
A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, m <= z -> n0 <= m -> A m:t -> Prop
left_step:=forall n0 : t, n0 < z -> A (S n0) -> A n0:Prop
left_step':=forall n0 : t,
n0 <= z -> A' (S n0) -> A n0:Prop
left_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
R:forall n0 : t, z <= n0 -> A n0
L:left_step'
n:t
H:z < n
A n
-A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, m <= z -> n0 <= m -> A m:t -> Prop
left_step:=forall n0 : t, n0 < z -> A (S n0) -> A n0:Prop
left_step':=forall n0 : t,
n0 <= z -> A' (S n0) -> A n0:Prop
left_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
R:forall n0 : t, z <= n0 -> A n0
L:left_step'
n:t
H:n < z
A n apply strong_left_induction; auto.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, m <= z -> n0 <= m -> A m:t -> Prop
left_step:=forall n0 : t, n0 < z -> A (S n0) -> A n0:Prop
left_step':=forall n0 : t,
n0 <= z -> A' (S n0) -> A n0:Prop
left_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
R:forall n0 : t, z <= n0 -> A n0
L:left_step'
n:t
H:n < z
n <= z now apply lt_le_incl.
-A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, m <= z -> n0 <= m -> A m:t -> Prop
left_step:=forall n0 : t, n0 < z -> A (S n0) -> A n0:Prop
left_step':=forall n0 : t,
n0 <= z -> A' (S n0) -> A n0:Prop
left_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
R:forall n0 : t, z <= n0 -> A n0
L:left_step'
n:t
H:n == z
A n rewrite H; apply R; now apply eq_le_incl.
-A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A':=fun n0 : t =>
forall m : t, m <= z -> n0 <= m -> A m:t -> Prop
left_step:=forall n0 : t, n0 < z -> A (S n0) -> A n0:Prop
left_step':=forall n0 : t,
n0 <= z -> A' (S n0) -> A n0:Prop
left_step'':=forall n0 : t, A' n0 <-> A' (S n0):Prop
R:forall n0 : t, z <= n0 -> A n0
L:left_step'
n:t
H:z < n
A n apply R; now apply lt_le_incl.
Qed.

End LeftInduction.

Theorem order_induction :
  A z ->
  (forall n, z <= n -> A n -> A (S n)) ->
  (forall n, n < z  -> A (S n) -> A n) ->
    forall n, A n.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A z ->
(forall n : t, z <= n -> A n -> A (S n)) ->
(forall n : t, n < z -> A (S n) -> A n) ->
forall n : t, A n
Proof.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A z ->
(forall n : t, z <= n -> A n -> A (S n)) ->
(forall n : t, n < z -> A (S n) -> A n) ->
forall n : t, A n
intros Az RS LS n.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
Az:A z
RS:forall n0 : t, z <= n0 -> A n0 -> A (S n0)
LS:forall n0 : t, n0 < z -> A (S n0) -> A n0
n:t
A n
destruct (lt_trichotomy n z) as [H | [H | H]].A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
Az:A z
RS:forall n0 : t, z <= n0 -> A n0 -> A (S n0)
LS:forall n0 : t, n0 < z -> A (S n0) -> A n0
n:t
H:n < z
A n
A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
Az:A z
RS:forall n0 : t, z <= n0 -> A n0 -> A (S n0)
LS:forall n0 : t, n0 < z -> A (S n0) -> A n0
n:t
H:n == z
A n
A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
Az:A z
RS:forall n0 : t, z <= n0 -> A n0 -> A (S n0)
LS:forall n0 : t, n0 < z -> A (S n0) -> A n0
n:t
H:z < n
A n
-A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
Az:A z
RS:forall n0 : t, z <= n0 -> A n0 -> A (S n0)
LS:forall n0 : t, n0 < z -> A (S n0) -> A n0
n:t
H:n < z
A n now apply left_induction; [| | apply lt_le_incl].
-A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
Az:A z
RS:forall n0 : t, z <= n0 -> A n0 -> A (S n0)
LS:forall n0 : t, n0 < z -> A (S n0) -> A n0
n:t
H:n == z
A n now rewrite H.
-A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
Az:A z
RS:forall n0 : t, z <= n0 -> A n0 -> A (S n0)
LS:forall n0 : t, n0 < z -> A (S n0) -> A n0
n:t
H:z < n
A n now apply right_induction; [| | apply lt_le_incl].
Qed.

Theorem order_induction' :
  A z ->
  (forall n, z <= n -> A n -> A (S n)) ->
  (forall n, n <= z -> A n -> A (P n)) ->
    forall n, A n.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A z ->
(forall n : t, z <= n -> A n -> A (S n)) ->
(forall n : t, n <= z -> A n -> A (P n)) ->
forall n : t, A n
Proof.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
A z ->
(forall n : t, z <= n -> A n -> A (S n)) ->
(forall n : t, n <= z -> A n -> A (P n)) ->
forall n : t, A n
intros Az AS AP n; apply order_induction; try assumption.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
Az:A z
AS:forall n0 : t, z <= n0 -> A n0 -> A (S n0)
AP:forall n0 : t, n0 <= z -> A n0 -> A (P n0)
n:t
forall n0 : t, n0 < z -> A (S n0) -> A n0
intros m H1 H2.A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
Az:A z
AS:forall n0 : t, z <= n0 -> A n0 -> A (S n0)
AP:forall n0 : t, n0 <= z -> A n0 -> A (P n0)
n, m:t
H1:m < z
H2:A (S m)
A m apply AP in H2; [|now apply le_succ_l].A:t -> Prop
A_wd:Proper (eq ==> iff) A
z:t
Az:A z
AS:forall n0 : t, z <= n0 -> A n0 -> A (S n0)
AP:forall n0 : t, n0 <= z -> A n0 -> A (P n0)
n, m:t
H1:m < z
H2:A (P (S m))
A m
now rewrite pred_succ in H2.
Qed.

End Center.

Theorem order_induction_0 :
  A 0 ->
  (forall n, 0 <= n -> A n -> A (S n)) ->
  (forall n, n < 0  -> A (S n) -> A n) ->
    forall n, A n.A:t -> Prop
A_wd:Proper (eq ==> iff) A
A 0 ->
(forall n : t, 0 <= n -> A n -> A (S n)) ->
(forall n : t, n < 0 -> A (S n) -> A n) ->
forall n : t, A n
Proof (order_induction 0).

Theorem order_induction'_0 :
  A 0 ->
  (forall n, 0 <= n -> A n -> A (S n)) ->
  (forall n, n <= 0 -> A n -> A (P n)) ->
    forall n, A n.A:t -> Prop
A_wd:Proper (eq ==> iff) A
A 0 ->
(forall n : t, 0 <= n -> A n -> A (S n)) ->
(forall n : t, n <= 0 -> A n -> A (P n)) ->
forall n : t, A n
Proof (order_induction' 0).

Elimintation principle for <

Theorem lt_ind : forall (n : t),
  A (S n) ->
  (forall m, n < m -> A m -> A (S m)) ->
   forall m, n < m -> A m.A:t -> Prop
A_wd:Proper (eq ==> iff) A
forall n : t,
A (S n) ->
(forall m : t, n < m -> A m -> A (S m)) ->
forall m : t, n < m -> A m
Proof.A:t -> Prop
A_wd:Proper (eq ==> iff) A
forall n : t,
A (S n) ->
(forall m : t, n < m -> A m -> A (S m)) ->
forall m : t, n < m -> A m
intros n H1 H2 m H3.A:t -> Prop
A_wd:Proper (eq ==> iff) A
n:t
H1:A (S n)
H2:forall m0 : t, n < m0 -> A m0 -> A (S m0)
m:t
H3:n < m
A m
apply right_induction with (S n); [assumption | | now apply le_succ_l].A:t -> Prop
A_wd:Proper (eq ==> iff) A
n:t
H1:A (S n)
H2:forall m0 : t, n < m0 -> A m0 -> A (S m0)
m:t
H3:n < m
forall n0 : t, S n <= n0 -> A n0 -> A (S n0)
intros; apply H2; try assumption.A:t -> Prop
A_wd:Proper (eq ==> iff) A
n:t
H1:A (S n)
H2:forall m0 : t, n < m0 -> A m0 -> A (S m0)
m:t
H3:n < m
n0:t
H:S n <= n0
H0:A n0
n < n0 now apply le_succ_l.
Qed.

Elimination principle for <=

Theorem le_ind : forall (n : t),
  A n ->
  (forall m, n <= m -> A m -> A (S m)) ->
   forall m, n <= m -> A m.A:t -> Prop
A_wd:Proper (eq ==> iff) A
forall n : t,
A n ->
(forall m : t, n <= m -> A m -> A (S m)) ->
forall m : t, n <= m -> A m
Proof.A:t -> Prop
A_wd:Proper (eq ==> iff) A
forall n : t,
A n ->
(forall m : t, n <= m -> A m -> A (S m)) ->
forall m : t, n <= m -> A m
intros n H1 H2 m H3.A:t -> Prop
A_wd:Proper (eq ==> iff) A
n:t
H1:A n
H2:forall m0 : t, n <= m0 -> A m0 -> A (S m0)
m:t
H3:n <= m
A m
now apply right_induction with n.
Qed.

End Induction.

Tactic Notation "nzord_induct" ident(n) :=
  induction_maker n ltac:(apply order_induction_0).

Tactic Notation "nzord_induct" ident(n) constr(z) :=
  induction_maker n ltac:(apply order_induction with z).

Section WF.

Variable z : t.

Let Rlt (n m : t) := z <= n < m.
Let Rgt (n m : t) := m < n <= z.

Instance Rlt_wd : Proper (eq ==> eq ==> iff) Rlt.z:t
Rlt:=fun n m : t => z <= n < m:t -> t -> Prop
Rgt:=fun n m : t => m < n <= z:t -> t -> Prop
Proper (eq ==> eq ==> iff) Rlt
Proof.z:t
Rlt:=fun n m : t => z <= n < m:t -> t -> Prop
Rgt:=fun n m : t => m < n <= z:t -> t -> Prop
Proper (eq ==> eq ==> iff) Rlt
intros x1 x2 H1 x3 x4 H2; unfold Rlt.z:t
Rlt:=fun n m : t => z <= n < m:t -> t -> Prop
Rgt:=fun n m : t => m < n <= z:t -> t -> Prop
x1, x2:t
H1:x1 == x2
x3, x4:t
H2:x3 == x4
z <= x1 < x3 <-> z <= x2 < x4 rewrite H1; now rewrite H2.
Qed.

Instance Rgt_wd : Proper (eq ==> eq ==> iff) Rgt.z:t
Rlt:=fun n m : t => z <= n < m:t -> t -> Prop
Rgt:=fun n m : t => m < n <= z:t -> t -> Prop
Proper (eq ==> eq ==> iff) Rgt
Proof.z:t
Rlt:=fun n m : t => z <= n < m:t -> t -> Prop
Rgt:=fun n m : t => m < n <= z:t -> t -> Prop
Proper (eq ==> eq ==> iff) Rgt
intros x1 x2 H1 x3 x4 H2; unfold Rgt; rewrite H1; now rewrite H2.
Qed.

Theorem lt_wf : well_founded Rlt.z:t
Rlt:=fun n m : t => z <= n < m:t -> t -> Prop
Rgt:=fun n m : t => m < n <= z:t -> t -> Prop
well_founded Rlt
Proof.z:t
Rlt:=fun n m : t => z <= n < m:t -> t -> Prop
Rgt:=fun n m : t => m < n <= z:t -> t -> Prop
well_founded Rlt
unfold well_founded.z:t
Rlt:=fun n m : t => z <= n < m:t -> t -> Prop
Rgt:=fun n m : t => m < n <= z:t -> t -> Prop
forall a : t, Acc Rlt a
apply strong_right_induction' with (z := z).z:t
Rlt:=fun n m : t => z <= n < m:t -> t -> Prop
Rgt:=fun n m : t => m < n <= z:t -> t -> Prop
Proper (eq ==> iff) (Acc Rlt)
z:t
Rlt:=fun n m : t => z <= n < m:t -> t -> Prop
Rgt:=fun n m : t => m < n <= z:t -> t -> Prop
forall n : t, n <= z -> Acc Rlt n
z:t
Rlt:=fun n m : t => z <= n < m:t -> t -> Prop
Rgt:=fun n m : t => m < n <= z:t -> t -> Prop
forall n : t,
z <= n ->
(forall m : t, z <= m -> m < n -> Acc Rlt m) ->
Acc Rlt n
-z:t
Rlt:=fun n m : t => z <= n < m:t -> t -> Prop
Rgt:=fun n m : t => m < n <= z:t -> t -> Prop
Proper (eq ==> iff) (Acc Rlt) auto with typeclass_instances.
-z:t
Rlt:=fun n m : t => z <= n < m:t -> t -> Prop
Rgt:=fun n m : t => m < n <= z:t -> t -> Prop
forall n : t, n <= z -> Acc Rlt n intros n H; constructor; intros y [H1 H2].z:t
Rlt:=fun n0 m : t => z <= n0 < m:t -> t -> Prop
Rgt:=fun n0 m : t => m < n0 <= z:t -> t -> Prop
n:t
H:n <= z
y:t
H1:z <= y
H2:y < n
Acc Rlt y
  apply nle_gt in H2.z:t
Rlt:=fun n0 m : t => z <= n0 < m:t -> t -> Prop
Rgt:=fun n0 m : t => m < n0 <= z:t -> t -> Prop
n:t
H:n <= z
y:t
H1:z <= y
H2:~ n <= y
Acc Rlt y elim H2.z:t
Rlt:=fun n0 m : t => z <= n0 < m:t -> t -> Prop
Rgt:=fun n0 m : t => m < n0 <= z:t -> t -> Prop
n:t
H:n <= z
y:t
H1:z <= y
H2:~ n <= y
n <= y now apply le_trans with z.
-z:t
Rlt:=fun n m : t => z <= n < m:t -> t -> Prop
Rgt:=fun n m : t => m < n <= z:t -> t -> Prop
forall n : t,
z <= n ->
(forall m : t, z <= m -> m < n -> Acc Rlt m) ->
Acc Rlt n intros n H1 H2; constructor; intros m [H3 H4].z:t
Rlt:=fun n0 m0 : t => z <= n0 < m0:t -> t -> Prop
Rgt:=fun n0 m0 : t => m0 < n0 <= z:t -> t -> Prop
n:t
H1:z <= n
H2:forall m0 : t, z <= m0 -> m0 < n -> Acc Rlt m0
m:t
H3:z <= m
H4:m < n
Acc Rlt m now apply H2.
Qed.

Theorem gt_wf : well_founded Rgt.z:t
Rlt:=fun n m : t => z <= n < m:t -> t -> Prop
Rgt:=fun n m : t => m < n <= z:t -> t -> Prop
well_founded Rgt
Proof.z:t
Rlt:=fun n m : t => z <= n < m:t -> t -> Prop
Rgt:=fun n m : t => m < n <= z:t -> t -> Prop
well_founded Rgt
unfold well_founded.z:t
Rlt:=fun n m : t => z <= n < m:t -> t -> Prop
Rgt:=fun n m : t => m < n <= z:t -> t -> Prop
forall a : t, Acc Rgt a
apply strong_left_induction' with (z := z).z:t
Rlt:=fun n m : t => z <= n < m:t -> t -> Prop
Rgt:=fun n m : t => m < n <= z:t -> t -> Prop
Proper (eq ==> iff) (Acc Rgt)
z:t
Rlt:=fun n m : t => z <= n < m:t -> t -> Prop
Rgt:=fun n m : t => m < n <= z:t -> t -> Prop
forall n : t, z <= n -> Acc Rgt n
z:t
Rlt:=fun n m : t => z <= n < m:t -> t -> Prop
Rgt:=fun n m : t => m < n <= z:t -> t -> Prop
forall n : t,
n <= z ->
(forall m : t, m <= z -> S n <= m -> Acc Rgt m) ->
Acc Rgt n
-z:t
Rlt:=fun n m : t => z <= n < m:t -> t -> Prop
Rgt:=fun n m : t => m < n <= z:t -> t -> Prop
Proper (eq ==> iff) (Acc Rgt) auto with typeclass_instances.
-z:t
Rlt:=fun n m : t => z <= n < m:t -> t -> Prop
Rgt:=fun n m : t => m < n <= z:t -> t -> Prop
forall n : t, z <= n -> Acc Rgt n intros n H; constructor; intros y [H1 H2].z:t
Rlt:=fun n0 m : t => z <= n0 < m:t -> t -> Prop
Rgt:=fun n0 m : t => m < n0 <= z:t -> t -> Prop
n:t
H:z <= n
y:t
H1:n < y
H2:y <= z
Acc Rgt y
  apply nle_gt in H2.z:t
Rlt:=fun n0 m : t => z <= n0 < m:t -> t -> Prop
Rgt:=fun n0 m : t => m < n0 <= z:t -> t -> Prop
n:t
H:z <= n
y:t
H1:n < y
H2:False
Acc Rgt y
z:t
Rlt:=fun n0 m : t => z <= n0 < m:t -> t -> Prop
Rgt:=fun n0 m : t => m < n0 <= z:t -> t -> Prop
n:t
H:z <= n
y:t
H1:n < y
H2:y <= z
H0:forall n0 m : t, m < n0 -> ~ n0 <= m
z < y
  +z:t
Rlt:=fun n0 m : t => z <= n0 < m:t -> t -> Prop
Rgt:=fun n0 m : t => m < n0 <= z:t -> t -> Prop
n:t
H:z <= n
y:t
H1:n < y
H2:False
Acc Rgt y elim H2.
  +z:t
Rlt:=fun n0 m : t => z <= n0 < m:t -> t -> Prop
Rgt:=fun n0 m : t => m < n0 <= z:t -> t -> Prop
n:t
H:z <= n
y:t
H1:n < y
H2:y <= z
H0:forall n0 m : t, m < n0 -> ~ n0 <= m
z < y now apply le_lt_trans with n.
-z:t
Rlt:=fun n m : t => z <= n < m:t -> t -> Prop
Rgt:=fun n m : t => m < n <= z:t -> t -> Prop
forall n : t,
n <= z ->
(forall m : t, m <= z -> S n <= m -> Acc Rgt m) ->
Acc Rgt n intros n H1 H2; constructor; intros m [H3 H4].z:t
Rlt:=fun n0 m0 : t => z <= n0 < m0:t -> t -> Prop
Rgt:=fun n0 m0 : t => m0 < n0 <= z:t -> t -> Prop
n:t
H1:n <= z
H2:forall m0 : t, m0 <= z -> S n <= m0 -> Acc Rgt m0
m:t
H3:n < m
H4:m <= z
Acc Rgt m
  apply H2.z:t
Rlt:=fun n0 m0 : t => z <= n0 < m0:t -> t -> Prop
Rgt:=fun n0 m0 : t => m0 < n0 <= z:t -> t -> Prop
n:t
H1:n <= z
H2:forall m0 : t, m0 <= z -> S n <= m0 -> Acc Rgt m0
m:t
H3:n < m
H4:m <= z
m <= z
z:t
Rlt:=fun n0 m0 : t => z <= n0 < m0:t -> t -> Prop
Rgt:=fun n0 m0 : t => m0 < n0 <= z:t -> t -> Prop
n:t
H1:n <= z
H2:forall m0 : t, m0 <= z -> S n <= m0 -> Acc Rgt m0
m:t
H3:n < m
H4:m <= z
S n <= m
  +z:t
Rlt:=fun n0 m0 : t => z <= n0 < m0:t -> t -> Prop
Rgt:=fun n0 m0 : t => m0 < n0 <= z:t -> t -> Prop
n:t
H1:n <= z
H2:forall m0 : t, m0 <= z -> S n <= m0 -> Acc Rgt m0
m:t
H3:n < m
H4:m <= z
m <= z assumption. +z:t
Rlt:=fun n0 m0 : t => z <= n0 < m0:t -> t -> Prop
Rgt:=fun n0 m0 : t => m0 < n0 <= z:t -> t -> Prop
n:t
H1:n <= z
H2:forall m0 : t, m0 <= z -> S n <= m0 -> Acc Rgt m0
m:t
H3:n < m
H4:m <= z
S n <= m now apply le_succ_l.
Qed.

End WF.

End NZOrderProp.

If we have moreover a compare function, we can build an OrderedType structure.

(* Temporary workaround for bug #2949: remove this problematic + unused functor
Module NZOrderedType (NZ : NZDecOrdSig')
 <: DecidableTypeFull <: OrderedTypeFull
 := NZ <+ NZBaseProp <+ NZOrderProp <+ Compare2EqBool <+ HasEqBool2Dec.
*)