Theorem: Image.n1_lt_n (Ray/Render/Image.lean)

State before:
n chunk : ℕ
h : ¬n ≤ max 1 chunk
⊢ n - n / 2 < n
Tactic:
simp only [le_max_iff] at h
State after:
n chunk : ℕ
h : ¬(n ≤ 1 ∨ n ≤ chunk)
⊢ n - n / 2 < n

State before:
n chunk : ℕ
h : ¬(n ≤ 1 ∨ n ≤ chunk)
⊢ n - n / 2 < n
Tactic:
omega
State after:
no goals