src/HOL/Library/Cancellation.thy

--- a/src/HOL/Library/Cancellation.thy	Wed May 10 19:02:06 2017 +0200
+++ b/src/HOL/Library/Cancellation.thy	Wed May 10 19:11:20 2017 +0200
@@ -39,7 +39,7 @@
   by (induction n) auto
 
 lemma iterate_add_1: \<open>iterate_add n 1 = of_nat n\<close>
-  by (induction n) auto
+  using iterate_add_Numeral1 by auto
 
 lemma iterate_add_eq_add_iff1:
   \<open>i \<le> j \<Longrightarrow> (iterate_add j u + m = iterate_add i u + n) = (iterate_add (j - i) u + m = n)\<close>