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

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

State before:
n : ℕ
h1 : n ≠ 0
h2 : n ≠ 1
h3 : 1 ≤ n
⊢ ∃ k, n = k + 2
Tactic:
have h4 : 2 ≤ n := lt_of_le_of_ne' h3 h2
State after:
n : ℕ
h1 : n ≠ 0
h2 : n ≠ 1
h3 : 1 ≤ n
h4 : 2 ≤ n
⊢ ∃ k, n = k + 2

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