src/HOL/Algebra/Divisibility.thy

           apply (simp, (fast intro: nth_mem[OF len])?)+
     done
 
     from len
       have as': "as' = (take i as' @ as'!i # drop (Suc i) as')"
-      by (simp add: drop_Suc_conv_tl)
+      by (simp add: Cons_nth_drop_Suc)
     with carr
       have eer: "essentially_equal G (take i as' @ as'!i # drop (Suc i) as') as'"
       by simp
     with v2 afs' carr aa1carr aa2carr nth_mem[OF len]
       have "aa_1 \<otimes> (as'!i \<otimes> aa_2) \<sim> a"