# HG changeset patch
# User haftmann
# Date 1534941178 0
# Node ID 134be95e57878f1ba7620df0a61f0faa66d95c89
# Parent  862b1288020f6f2cfc8d7170b4cb050f77bdae07
slightly generalized theorems

diff -r 862b1288020f -r 134be95e5787 src/HOL/Binomial.thy
--- a/src/HOL/Binomial.thy	Wed Aug 22 12:32:58 2018 +0000
+++ b/src/HOL/Binomial.thy	Wed Aug 22 12:32:58 2018 +0000
@@ -342,6 +342,12 @@
 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)
@@ -421,12 +427,6 @@
 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))"