rewrite [mul_comm]
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ n¡ / (k¡ * (n - k)¡) = n¡ / ((n - k)¡ * (n - (n - k))¡)
n k : ℕ
hn : n ≠ 0
hk : k ≠ 0
hnk : n - k ≠ 0
⊢ n¡ / ((n - k)¡ * k¡) = n¡ / ((n - k)¡ * (n - (n - k))¡)