Theorem: HTPI.exists_eq_add_one_of_ne_zero (HTPILib/Chap6.lean)

State before:
n : ℕ
h1 : n ≠ 0
⊢ ∃ k, n = k + 1
Tactic:
have h2 : 1 ≤ n := Nat.pos_of_ne_zero h1
State after:
n : ℕ
h1 : n ≠ 0
h2 : 1 ≤ n
⊢ ∃ k, n = k + 1

State before:
n : ℕ
h1 : n ≠ 0
h2 : 1 ≤ n
⊢ ∃ k, n = k + 1
Tactic:
show ∃ (k : Nat), n = k + 1 from Nat.exists_eq_add_of_le' h2
State after:
no goals