[STATEMENT]
lemma gbinomial_int_mult_fact: "fact k * (a gchoose k) = (\<Prod>i = 0..<k. a - int i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fact k * (a gchoose k) = (\<Prod>i = 0..<k. a - int i)
[PROOF STEP]
by (simp only: gbinomial_int_pochhammer' fact_dvd_pochhammer dvd_mult_div_cancel falling_fact_pochhammer')