Theorem nat_strong_induction

Proof
let C n ↔ (∀k. k ∈ ℕ → k ≤ n → P k).
01. 1 ⊢ P 0, hypo.
02. 2 ⊢ ∀n. n ∈ ℕ → C n → P (n + 1), hypo.
03. 3 ⊢ k ∈ ℕ, hypo.
04. 4 ⊢ k ≤ 0, hypo.
05. 3 ⊢ 0 ≤ k, nat_non_negative 3.
06. ⊢ 0 ∈ ℕ, zero_in_nat.
07. 3, 4 ⊢ k = 0, nle_antisym 3 6 4 5.
08. 1, 3, 4 ⊢ P k, eq_subst_rev 7 1, P t ↔ P t.
09. 1 ⊢ k ∈ ℕ → k ≤ 0 → P k, subj_intro_ii 8.
10. 1 ⊢ C 0, uq_intro 9.

11. 11 ⊢ n ∈ ℕ, hypo.
12. 12 ⊢ C n, hypo.
13. 2, 11 ⊢ C n → P (n + 1), uq_bounded_elim 2 11.
14. 2, 11, 12 ⊢ P (n + 1), subj_elim 13 12.
15. 15 ⊢ k ∈ ℕ, hypo.
16. 16 ⊢ k ≤ n + 1, hypo.
17. 11, 15, 16 ⊢ k ≤ n ∨ k = n + 1, nle_succ_split 15 11 16.
18. 18 ⊢ k ≤ n, hypo.
19. 12, 15 ⊢ k ≤ n → P k, uq_bounded_elim 12 15.
20. 12, 15, 18 ⊢ P k, subj_elim 19 18.
21. 21 ⊢ k = n + 1, hypo.
22. 2, 11, 12, 21 ⊢ P k, eq_subst_rev 21 14, P t ↔ P t.
23. 2, 11, 12, 15, 16 ⊢ P k, disj_elim 17 20 22.
24. 2, 11, 12 ⊢ k ∈ ℕ → k ≤ n + 1 → P k, subj_intro_ii 23.
25. 2, 11, 12 ⊢ C (n + 1), uq_intro 24.
26. 2 ⊢ n ∈ ℕ → C n → C (n + 1), subj_intro_ii 25.
27. 2 ⊢ ∀n. n ∈ ℕ → C n → C (n + 1), uq_intro 26.

28. 1, 2 ⊢ ∀n. n ∈ ℕ → C n, nat_induction 10 27, P n ↔ C n.
29. 29 ⊢ n ∈ ℕ, hypo.
30. 1, 2, 29 ⊢ C n, uq_bounded_elim 28 29.
31. 1, 2, 29 ⊢ n ≤ n → P n, uq_bounded_elim 30 29.
32. 29 ⊢ n ≤ n, nle_refl 29.
33. 1, 2, 29 ⊢ P n, subj_elim 31 32.
34. 1, 2 ⊢ n ∈ ℕ → P n, subj_intro 33.
35. 1, 2 ⊢ ∀n. n ∈ ℕ → P n, uq_intro 34.
nat_strong_induction. ⊢ P 0 →
  (∀n. n ∈ ℕ → (∀k. k ∈ ℕ → k ≤ n → P k) → P (n + 1)) →
  (∀n. n ∈ ℕ → P n), subj_intro_ii 35.

Dependencies
The given proof depends on 18 axioms:
comp, efq, eq_refl, eq_subst, ext, lem, radd_assoc, radd_closed, radd_inv, radd_neutr, real_is_set, rle_antisym, rle_compat_add, rle_refl, rle_total, rle_trans, rneg_closed, subset.