no goals
n k s : ℕ
hkn : k ≤ n
hsk : s ≤ k
⊢ (n - k)! * (k - s)! * s ! ≠ 0
apply_rules [factorial_ne_zero, mul_ne_zero]
no goals
n k s : ℕ
hkn : k ≤ n
hsk : s ≤ k
h : (n - k)! * (k - s)! * s ! ≠ 0
⊢ choose n k * choose k s * ((n - k)! * (k - s)! * s !) = choose n k * (choose k s * s ! * (k - s)!) * (n - k)!
rw [mul_assoc, mul_assoc, mul_assoc, mul_assoc _ s !, mul_assoc, mul_comm (n - k)!,
mul_comm s !]
no goals
n k s : ℕ
hkn : k ≤ n
hsk : s ≤ k
h : (n - k)! * (k - s)! * s ! ≠ 0
⊢ choose n k * (choose k s * s ! * (k - s)!) * (n - k)! = n !
rw [choose_mul_factorial_mul_factorial hsk, choose_mul_factorial_mul_factorial hkn]
no goals
n k s : ℕ
hkn : k ≤ n
hsk : s ≤ k
h : (n - k)! * (k - s)! * s ! ≠ 0
⊢ n ! = choose n s * s ! * (choose (n - s) (k - s) * (k - s)! * (n - s - (k - s))!)
rw [choose_mul_factorial_mul_factorial (tsub_le_tsub_right hkn _),
choose_mul_factorial_mul_factorial (hsk.trans hkn)]
no goals
n k s : ℕ
hkn : k ≤ n
hsk : s ≤ k
h : (n - k)! * (k - s)! * s ! ≠ 0
⊢ choose n s * s ! * (choose (n - s) (k - s) * (k - s)! * (n - s - (k - s))!) =
    choose n s * choose (n - s) (k - s) * ((n - k)! * (k - s)! * s !)
rw [tsub_tsub_tsub_cancel_right hsk, mul_assoc, mul_left_comm s !, mul_assoc,
mul_comm (k - s)!, mul_comm s !, mul_right_comm, ← mul_assoc]