rw [← not_le]
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
h2 : ∑ i ∈ Finset.range n, i < k
⊢ n < 6
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
h2 : ∑ i ∈ Finset.range n, i < k
⊢ ¬6 ≤ n