# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1722246557 -3600
# Node ID 424b90ba7b6ff24d6e7ef09011ff8e558a412a47
# Parent  0c4d17ef855d5dc7838e84368086cdbda5d28774
Further divide_mono fixes

diff -r 0c4d17ef855d -r 424b90ba7b6f src/HOL/Analysis/Improper_Integral.thy
--- a/src/HOL/Analysis/Improper_Integral.thy	Mon Jul 29 10:24:54 2024 +0100
+++ b/src/HOL/Analysis/Improper_Integral.thy	Mon Jul 29 10:49:17 2024 +0100
@@ -959,9 +959,8 @@
               by (simp add: dist_norm norm_minus_commute)
             also have "... \<le> \<epsilon> * (b \<bullet> i - a \<bullet> i) / \<bar>v \<bullet> i - u \<bullet> i\<bar> / (4 * content (cbox a b))"
             proof (intro mult_right_mono divide_left_mono divide_right_mono uvi)
-              show "norm (v - u) * \<bar>v \<bullet> i - u \<bullet> i\<bar> > 0"
-                using u_less_v [OF \<open>i \<in> Basis\<close>] 
-                by (auto simp: less_eq_real_def zero_less_mult_iff that)
+              show "\<bar>v \<bullet> i - u \<bullet> i\<bar> > 0"
+                using u_less_v [OF \<open>i \<in> Basis\<close>] by force 
               show "\<epsilon> * (b \<bullet> i - a \<bullet> i) \<ge> 0"
                 using a_less_b \<open>0 < \<epsilon>\<close> \<open>i \<in> Basis\<close> by force
             qed auto
diff -r 0c4d17ef855d -r 424b90ba7b6f src/HOL/Decision_Procs/Approximation_Bounds.thy
--- a/src/HOL/Decision_Procs/Approximation_Bounds.thy	Mon Jul 29 10:24:54 2024 +0100
+++ b/src/HOL/Decision_Procs/Approximation_Bounds.thy	Mon Jul 29 10:49:17 2024 +0100
@@ -956,13 +956,14 @@
       using bnds_sqrt'[of ?sxx prec] by auto
     finally
     have "sqrt (1 + x*x) \<le> ub_sqrt prec ?sxx" .
-    hence "?R \<le> ?fR" by (auto simp: float_plus_up.rep_eq plus_up_def intro!: truncate_up_le)
+    hence \<dagger>: "?R \<le> ?fR" by (auto simp: float_plus_up.rep_eq plus_up_def intro!: truncate_up_le)
     hence "0 < ?fR" and "0 < real_of_float ?fR" using \<open>0 < ?R\<close> by auto
 
     have monotone: "?DIV \<le> x / ?R"
     proof -
       have "?DIV \<le> real_of_float x / ?fR" by (rule float_divl)
-      also have "\<dots> \<le> x / ?R" by (rule divide_left_mono[OF \<open>?R \<le> ?fR\<close> \<open>0 \<le> real_of_float x\<close> mult_pos_pos[OF order_less_le_trans[OF divisor_gt0 \<open>?R \<le> real_of_float ?fR\<close>] divisor_gt0]])
+      also have "\<dots> \<le> x / ?R"
+        by (simp add: \<dagger> assms divide_left_mono divisor_gt0)
       finally show ?thesis .
     qed
 
@@ -1081,16 +1082,16 @@
     also have "\<dots> \<le> sqrt (1 + x*x)"
       by (auto simp: float_plus_down.rep_eq plus_down_def float_round_down.rep_eq truncate_down_le)
     finally have "lb_sqrt prec ?sxx \<le> sqrt (1 + x*x)" .
-    hence "?fR \<le> ?R"
+    hence \<dagger>: "?fR \<le> ?R"
       by (auto simp: float_plus_down.rep_eq plus_down_def truncate_down_le)
+    have monotone: "x / ?R \<le> (float_divr prec x ?fR)"
+    proof -
     have "0 < real_of_float ?fR"
       by (auto simp: float_plus_down.rep_eq plus_down_def float_round_down.rep_eq
         intro!: truncate_down_ge1 lb_sqrt_lower_bound order_less_le_trans[OF zero_less_one]
         truncate_down_nonneg add_nonneg_nonneg)
-    have monotone: "x / ?R \<le> (float_divr prec x ?fR)"
-    proof -
-      from divide_left_mono[OF \<open>?fR \<le> ?R\<close> \<open>0 \<le> real_of_float x\<close> mult_pos_pos[OF divisor_gt0 \<open>0 < real_of_float ?fR\<close>]]
-      have "x / ?R \<le> x / ?fR" .
+      then have "x / ?R \<le> x / ?fR"
+        using \<dagger> assms divide_left_mono by blast 
       also have "\<dots> \<le> ?DIV" by (rule float_divr)
       finally show ?thesis .
     qed