src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy

     also have "\<dots> = (Ipoly bs p) ^ (Suc n div 2 + Suc n div 2 + 1)"
       by (simp only: power_add power_one_right) simp
     also have "\<dots> = (Ipoly bs p) ^ (Suc (Suc (Suc 0) * (Suc n div Suc (Suc 0))))"
       by (simp only: th)
     finally have ?case unfolding numeral_2_eq_2 [symmetric]
-    using odd_two_times_div_two_Suc [OF odd] by simp
+    using odd_two_times_div_two_nat [OF odd] by simp
   }
   moreover
   {
     assume even: "even (Suc n)"
     from even have "Ipoly bs (p ^\<^sub>p Suc n) = Ipoly bs ?d"