[STATEMENT]
lemma binomial_gbinomial: "of_nat (n choose k) = (of_nat n gchoose k :: 'a::field_char_0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_nat (n choose k) = of_nat n gchoose k
[PROOF STEP]
by (simp add: gbinomial_binomial [symmetric] of_nat_gbinomial)