diff -r 68def9274939 -r b249fab48c76 src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Fri Apr 27 12:43:05 2018 +0100
+++ b/src/HOL/Set_Interval.thy	Wed May 02 12:47:56 2018 +0100
@@ -2459,6 +2459,17 @@
   finally show ?thesis .
 qed
 
+lemma prod_nat_group: "(\<Prod>m<n::nat. prod f {m * k ..< m*k + k}) = prod f {..< n * k}"
+proof (cases "k = 0")
+  case True
+  then show ?thesis
+    by auto
+next
+  case False
+  then show ?thesis 
+    by (induct "n"; simp add: prod.atLeastLessThan_concat algebra_simps atLeast0_lessThan_Suc atLeast0LessThan[symmetric])
+qed
+
 
 subsection \<open>Efficient folding over intervals\<close>