# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1722266525 -3600
# Node ID 15a81ed33d2adc24479e7dc66310e714ee7823fa
# Parent  424b90ba7b6ff24d6e7ef09011ff8e558a412a47
Reversed my brain-dead stupid change to divide_left_mono and divide_left_mono_neg

diff -r 424b90ba7b6f -r 15a81ed33d2a src/HOL/Analysis/Improper_Integral.thy
--- a/src/HOL/Analysis/Improper_Integral.thy	Mon Jul 29 10:49:17 2024 +0100
+++ b/src/HOL/Analysis/Improper_Integral.thy	Mon Jul 29 16:22:05 2024 +0100
@@ -959,8 +959,9 @@
               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 "\<bar>v \<bullet> i - u \<bullet> i\<bar> > 0"
-                using u_less_v [OF \<open>i \<in> Basis\<close>] by force 
+              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 "\<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 424b90ba7b6f -r 15a81ed33d2a src/HOL/Decision_Procs/Approximation_Bounds.thy
--- a/src/HOL/Decision_Procs/Approximation_Bounds.thy	Mon Jul 29 10:49:17 2024 +0100
+++ b/src/HOL/Decision_Procs/Approximation_Bounds.thy	Mon Jul 29 16:22:05 2024 +0100
@@ -956,14 +956,13 @@
       using bnds_sqrt'[of ?sxx prec] by auto
     finally
     have "sqrt (1 + x*x) \<le> ub_sqrt prec ?sxx" .
-    hence \<dagger>: "?R \<le> ?fR" by (auto simp: float_plus_up.rep_eq plus_up_def intro!: truncate_up_le)
+    hence "?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 (simp add: \<dagger> assms divide_left_mono divisor_gt0)
+      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]])
       finally show ?thesis .
     qed
 
@@ -1082,16 +1081,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 \<dagger>: "?fR \<le> ?R"
+    hence "?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)
-      then have "x / ?R \<le> x / ?fR"
-        using \<dagger> assms divide_left_mono by blast 
+    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" .
       also have "\<dots> \<le> ?DIV" by (rule float_divr)
       finally show ?thesis .
     qed
diff -r 424b90ba7b6f -r 15a81ed33d2a src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Mon Jul 29 10:49:17 2024 +0100
+++ b/src/HOL/Fields.thy	Mon Jul 29 16:22:05 2024 +0100
@@ -949,7 +949,7 @@
   by (auto simp: field_simps zero_less_mult_iff mult_strict_right_mono)
 
 lemma divide_left_mono:
-  "\<lbrakk>b \<le> a; 0 \<le> c; 0 < b\<rbrakk> \<Longrightarrow> c / a \<le> c / b"
+  "\<lbrakk>b \<le> a; 0 \<le> c; 0 < a*b\<rbrakk> \<Longrightarrow> c / a \<le> c / b"
   by (auto simp: field_simps zero_less_mult_iff mult_right_mono)
 
 lemma divide_strict_left_mono_neg:
@@ -1156,7 +1156,7 @@
 lemma divide_right_mono_neg: "a \<le> b \<Longrightarrow> c \<le> 0 \<Longrightarrow> b / c \<le> a / c"
   by (auto dest: divide_right_mono [of _ _ "- c"])
 
-lemma divide_left_mono_neg: "a \<le> b \<Longrightarrow> c \<le> 0 \<Longrightarrow> 0 < a \<Longrightarrow> c / a \<le> c / b"
+lemma divide_left_mono_neg: "a \<le> b \<Longrightarrow> c \<le> 0 \<Longrightarrow> 0 < a * b \<Longrightarrow> c / a \<le> c / b"
   by (auto simp add: mult.commute dest: divide_left_mono [of _ _ "- c"])
 
 lemma inverse_le_iff: "inverse a \<le> inverse b \<longleftrightarrow> (0 < a * b \<longrightarrow> b \<le> a) \<and> (a * b \<le> 0 \<longrightarrow> a \<le> b)"