src/HOL/Computational_Algebra/Polynomial_Factorial.thy

     then have "(r + q * p) div p = q + r div p"
       by (rule div_poly_eq)
     with that show ?thesis
       by (cases "r = 0") (simp_all add: euclidean_size_poly_def div_poly_less ac_simps)
   qed
-qed (auto simp: euclidean_size_poly_def Rings.div_mult_mod_eq div_poly_less degree_mult_eq intro!: degree_mod_less' degree_mult_right_le
-    split: if_splits)
+qed (auto simp: euclidean_size_poly_def Rings.div_mult_mod_eq div_poly_less degree_mult_eq power_add
+    intro!: degree_mod_less' split: if_splits)
 
 end
 
 instance poly :: ("{field, normalization_euclidean_semiring, factorial_ring_gcd}") euclidean_ring_gcd
   by (rule euclidean_ring_gcd_class.intro, rule factorial_euclidean_semiring_gcdI) standard