src/HOL/Analysis/Henstock_Kurzweil_Integration.thy

--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Mon Mar 30 10:35:10 2020 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Tue Mar 31 15:51:15 2020 +0200
@@ -1526,7 +1526,7 @@
     apply (rule sum.cong)
     using assms
     apply simp
-    apply (metis abs_of_nonneg assms(1) content_pos_le division_ofD(4))
+    apply (metis abs_of_nonneg content_pos_le)
     done
   have e: "0 \<le> e"
     using assms(2) norm_ge_zero order_trans by blast