exact le_sum
case bc.hab.bc
k n : ℕ
hk : k > 0
n' : ℕ
hn' : 6 ≤ n'
IH : 2 ^ (n' * n') < (∑ i ∈ Finset.range n', i)!
A : ℕ := ∑ i ∈ Finset.range n', i
le_sum : ∑ i ∈ Finset.range 6, i ≤ A
⊢ 15 ≤ A
no goals