rw [← PartENat.coe_lt_coe, ← this]
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
this : multiplicity 2 ↑k ! = ↑(∑ i ∈ Finset.range n, i)
⊢ ∑ i ∈ Finset.range n, i < k
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
this : multiplicity 2 ↑k ! = ↑(∑ i ∈ Finset.range n, i)
⊢ multiplicity 2 ↑k ! < ↑k