Theorem nat_succ_le_from_lt

Proof
let A n ↔ (∀k. k ∈ ℕ → n < k → n + 1 ≤ k).
01. 1 ⊢ k ∈ ℕ, hypo.
02. 2 ⊢ 0 < k, hypo.
03. 2 ⊢ ¬0 = k, neq_from_lt 2.
04. 2 ⊢ ¬k = 0, neq_symm 3.
05. 1, 2 ⊢ ∃m. m ∈ ℕ ∧ k = m + 1, nat_non_zero_is_succ 1 4.
06. 6 ⊢ m ∈ ℕ ∧ k = m + 1, hypo.
07. 6 ⊢ m ∈ ℕ, conj_eliml 6.
08. 6 ⊢ k = m + 1, conj_elimr 6.
09. 6 ⊢ 0 ≤ m, nat_non_negative 7.
10. ⊢ 0 ∈ ℕ, calc.
11. ⊢ 1 ∈ ℕ, calc.
12. 6 ⊢ 0 + 1 ≤ m + 1, nle_compat_add 10 7 11 9.
13. 6 ⊢ m + 1 = k, eq_symm 8.
14. 6 ⊢ 0 + 1 ≤ k, le_eq_trans 12 13.
15. 1, 2 ⊢ 0 + 1 ≤ k, ex_elim 5 14.
16. ⊢ k ∈ ℕ → 0 < k → 0 + 1 ≤ k, subj_intro_ii 15.
17. ⊢ A 0, uq_intro 16.

18. 18 ⊢ n ∈ ℕ, hypo.
19. 19 ⊢ A n, hypo.
20. 20 ⊢ k ∈ ℕ, hypo.
21. 21 ⊢ n + 1 < k, hypo.
22. 18 ⊢ 0 ≤ n, nat_non_negative 18.
23. 18 ⊢ 0 + 1 ≤ n + 1, nle_compat_add 10 18 11 22.
24. ⊢ 1 = 0 + 1, calc.
25. 18 ⊢ 1 ≤ n + 1, eq_le_trans 24 23.
26. 18 ⊢ n + 1 ∈ ℕ, succ_in_nat 18.
27. 18, 20, 21 ⊢ 1 < k, nle_lt_trans 11 26 20 25 21.
28. ⊢ 0 < 1, calc.
29. 18, 20, 21 ⊢ 0 < k, nlt_lt_trans 10 11 20 28 27.
30. 18, 20, 21 ⊢ ¬0 = k, neq_from_lt 29.
31. 18, 20, 21 ⊢ ¬k = 0, neq_symm 30.
32. 18, 20, 21 ⊢ ∃m. m ∈ ℕ ∧ k = m + 1, nat_non_zero_is_succ 20 31.
33. 33 ⊢ m ∈ ℕ ∧ k = m + 1, hypo.
34. 33 ⊢ m ∈ ℕ, conj_eliml 33.
35. 33 ⊢ k = m + 1, conj_elimr 33.
36. 19, 33 ⊢ n < m → n + 1 ≤ m, uq_bounded_elim 19 34.
37. 21, 33 ⊢ n + 1 < m + 1, eq_subst 35 21, P t ↔ n + 1 < t.
38. 18, 21, 33 ⊢ n < m, nlt_add_cancel_rr 18 34 11 37.
39. 18, 19, 21, 33 ⊢ n + 1 ≤ m, subj_elim 36 38.
40. 18 ⊢ n + 1 ∈ ℕ, succ_in_nat 18.
41. 18, 19, 21, 33 ⊢ n + 1 + 1 ≤ m + 1, nle_compat_add 40 34 11 39.
42. 18, 19, 21, 33 ⊢ n + 1 + 1 ≤ k,
  eq_subst_rev 35 41, P t ↔ n + 1 + 1 ≤ t.
43. 18, 19, 20, 21 ⊢ n + 1 + 1 ≤ k, ex_elim 32 42.
44. 18, 19 ⊢ k ∈ ℕ → n + 1 < k → n + 1 + 1 ≤ k, subj_intro_ii 43.
45. 18, 19 ⊢ A (n + 1), uq_intro 44.
46. ⊢ n ∈ ℕ → A n → A (n + 1), subj_intro_ii 45.
47. ⊢ ∀n. n ∈ ℕ → A n → A (n + 1), uq_intro 46.

48. ⊢ ∀n. n ∈ ℕ → A n, nat_induction 17 47, P n ↔ A n.
49. 49 ⊢ n ∈ ℕ, hypo.
50. 50 ⊢ k ∈ ℕ, hypo.
51. 49 ⊢ A n, uq_bounded_elim 48 49.
52. 49, 50 ⊢ n < k → n + 1 ≤ k, uq_bounded_elim 51 50.
nat_succ_le_from_lt. ⊢ n ∈ ℕ → k ∈ ℕ → n < k → n + 1 ≤ k,
  subj_intro_ii 52.

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