src/HOL/Library/Formal_Power_Series.thy

 ultimately show ?thesis by (cases k, auto)
 qed
 *)
 
 lemma fps_divide_1 [simp]: "(a :: 'a::field fps) / 1 = a"
-  by (fact divide_1)
+  by (fact div_by_1)
 
 lemma radical_divide:
   fixes a :: "'a::field_char_0 fps"
   assumes kp: "k > 0"
     and ra0: "(r k (a $ 0)) ^ k = a $ 0"