Require Import Lt.
Require Import Le.

Definition lt_hereditary (P : nat → Prop) :=
  ∀ n : nat, (∀ m : nat, m < n → P m) → P n.

Lemma le_split : ∀ m n : nat, m ≤ S n → m ≤ n ∨ m = S n.
Proof.
intros m n H; elim (le_lt_or_eq m (S n)); auto with arith.
Qed.

Lemma course_of_values :
 ∀ P : nat → Prop, lt_hereditary P → ∀ n m : nat, m ≤ n → P m.
Proof.
unfold lt_hereditary in |- *; simple induction n.
intros; apply H.
elim (le_n_O_eq m); trivial with arith.
intros p abs; elim lt_n_O with p; trivial with arith.
intros p lemp m lemSp; elim le_split with m p; auto with arith.
intro E; rewrite E; auto with arith. Qed.

Lemma complete_induction :
 ∀ P : nat → Prop, lt_hereditary P → ∀ n : nat, P n.
Proof.
intros; apply course_of_values with (m := n) (n := n); auto with arith.
Qed.

Lemma nat_wf_ind :
 ∀ P : nat → Prop,
 P 0 →
 (∀ k : nat, (∀ l : nat, l ≤ k → P l) → P (S k)) →
 ∀ n : nat, P n.
Proof.
intros P H0 Hk.
cut (∀ n k : nat, k ≤ n → P k).
intros HC n.
apply HC with (n := n); auto with arith.
simple induction n.
intros k Def_k.
elimtype (0 = k); auto with arith.
clear n.
intros n Hn k k_le_Sn.
elim (le_split k n); auto with arith.
intro Def_k.
rewrite Def_k.
auto with arith.
Qed.