Theorem: HTPI.I_max (HTPILib/Chap8Part1.lean)

State before:
n : ℕ
⊢ n ∈ I (n + 1)
Tactic:
define
State after:
n : ℕ
⊢ n < n + 1

State before:
n : ℕ
⊢ n < n + 1
Tactic:
linarith
State after:
no goals