src/HOL/Number_Theory/Polynomial_Factorial.thy

   fixes a b :: "'a::field"
   assumes "b \<noteq> 0"
   shows "irreducible [:a,b:]"
 proof (rule irreducibleI)
   fix p q assume pq: "[:a,b:] = p * q"
-  also from this assms have "degree \<dots> = degree p + degree q" 
+  also from pq assms have "degree \<dots> = degree p + degree q" 
     by (intro degree_mult_eq) auto
   finally have "degree p = 0 \<or> degree q = 0" using assms by auto
   with assms pq show "is_unit p \<or> is_unit q"
     by (auto simp: is_unit_const_poly_iff dvd_field_iff elim!: degree_eq_zeroE)
 qed (insert assms, auto simp: is_unit_poly_iff)