src/HOL/Analysis/ex/Approximations.thy

 qed
 
 lemma euler_approx_aux_Suc:
   "euler_approx_aux (Suc m) = 1 + Suc m * euler_approx_aux m"
   unfolding euler_approx_aux_def
-  by (subst sum_distrib_left) (simp add: atLeastAtMostSuc_conv)
+  by (subst sum_distrib_left) (simp add: atLeastAtMostSuc_conv mult.commute)
 
 lemma eval_euler_approx_aux:
   "euler_approx_aux 0 = 1"
   "euler_approx_aux 1 = 2"
   "euler_approx_aux (Suc 0) = 2"
   "euler_approx_aux (numeral n) = 1 + numeral n * euler_approx_aux (pred_numeral n)" (is "?th")
 proof -
   have A: "euler_approx_aux (Suc m) = 1 + Suc m * euler_approx_aux m" for m :: nat
     unfolding euler_approx_aux_def
-    by (subst sum_distrib_left) (simp add: atLeastAtMostSuc_conv)
+    by (subst sum_distrib_left) (simp add: atLeastAtMostSuc_conv mult.commute)
   show ?th by (subst numeral_eq_Suc, subst A, subst numeral_eq_Suc [symmetric]) simp
 qed (simp_all add: euler_approx_aux_def)
 
 lemma euler_approx_aux_code [code]:
   "euler_approx_aux n = (if n = 0 then 1 else 1 + n * euler_approx_aux (n - 1))"