nle_succ_split

Theorem nle_succ_split

Theorem. nle_succ_split
k ∈ ℕ → n ∈ ℕ → k ≤ n + 1 → k ≤ n ∨ k = n + 1

Proof
01. 1 ⊢ k ∈ ℕ, hypo.
02. 2 ⊢ n ∈ ℕ, hypo.
03. 3 ⊢ k ≤ n + 1, hypo.
04. 1, 2 ⊢ k ≤ n ∨ n < k, nle_lt_tricho 1 2.
05. 5 ⊢ k ≤ n, hypo.
06. 5 ⊢ k ≤ n ∨ k = n + 1, disj_introl 5.
07. 7 ⊢ n < k, hypo.
08. 1, 2, 7 ⊢ n + 1 ≤ k, nat_succ_le_from_lt 2 1 7.
09. 2 ⊢ n + 1 ∈ ℕ, succ_in_nat 2.
10. 1, 2, 3, 7 ⊢ k = n + 1, nle_antisym 1 9 3 8.
11. 1, 2, 3, 7 ⊢ k ≤ n ∨ k = n + 1, disj_intror 10.
12. 1, 2, 3 ⊢ k ≤ n ∨ k = n + 1, disj_elim 4 6 11.
nle_succ_split. ⊢ k ∈ ℕ → n ∈ ℕ → k ≤ n + 1 → k ≤ n ∨ k = n + 1,
  subj_intro_iii 12.

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.