src/HOL/Binomial.thy

   by (simp_all add: gbinomial_prod_rev prod.atLeast0_lessThan_Suc_shift)
 
 lemma gbinomial_Suc: "a gchoose (Suc k) = prod (\<lambda>i. a - of_nat i) {0..k} div fact (Suc k)"
   by (simp add: gbinomial_prod_rev atLeastLessThanSuc_atLeastAtMost)
 
+lemma gbinomial_1 [simp]: "a gchoose 1 = a"
+  by (simp add: gbinomial_prod_rev lessThan_Suc)
+
+lemma gbinomial_Suc0 [simp]: "a gchoose Suc 0 = a"
+  by (simp add: gbinomial_prod_rev lessThan_Suc)
+
 lemma gbinomial_mult_fact: "fact n * (a gchoose n) = (\<Prod>i = 0..<n. a - of_nat i)"
   for a :: "'a::field_char_0"
   by (simp_all add: gbinomial_prod_rev field_simps)
 
 lemma gbinomial_mult_fact': "(a gchoose n) * fact n = (\<Prod>i = 0..<n. a - of_nat i)"

 lemma binomial_gbinomial: "of_nat (n choose k) = (of_nat n gchoose k :: 'a::field_char_0)"
   by (simp add: gbinomial_binomial [symmetric] of_nat_gbinomial)
 
 setup
   \<open>Sign.add_const_constraint (@{const_name gbinomial}, SOME @{typ "'a::field_char_0 \<Rightarrow> nat \<Rightarrow> 'a"})\<close>
-
-lemma gbinomial_1[simp]: "a gchoose 1 = a"
-  by (simp add: gbinomial_prod_rev lessThan_Suc)
-
-lemma gbinomial_Suc0[simp]: "a gchoose (Suc 0) = a"
-  by (simp add: gbinomial_prod_rev lessThan_Suc)
 
 lemma gbinomial_mult_1:
   fixes a :: "'a::field_char_0"
   shows "a * (a gchoose n) = of_nat n * (a gchoose n) + of_nat (Suc n) * (a gchoose (Suc n))"
   (is "?l = ?r")