let A := ∑ i ∈ Finset.range n', i
case calc_2.succ
k n : ℕ
hk : k > 0
n' : ℕ
hn' : 6 ≤ n'
IH : 2 ^ (n' * n') < (∑ i ∈ Finset.range n', i)!
⊢ 2 ^ ((n' + 1) * (n' + 1)) < (∑ i ∈ Finset.range (n' + 1), i)!
case calc_2.succ
k n : ℕ
hk : k > 0
n' : ℕ
hn' : 6 ≤ n'
IH : 2 ^ (n' * n') < (∑ i ∈ Finset.range n', i)!
A : ℕ := ∑ i ∈ Finset.range n', i
⊢ 2 ^ ((n' + 1) * (n' + 1)) < (∑ i ∈ Finset.range (n' + 1), i)!