src/HOL/OrderedGroup.thy
changeset 25230 022029099a83
parent 25194 37a1743f0fc3
child 25267 1f745c599b5c
     1.1 --- a/src/HOL/OrderedGroup.thy	Mon Oct 29 17:08:01 2007 +0100
     1.2 +++ b/src/HOL/OrderedGroup.thy	Tue Oct 30 08:45:54 2007 +0100
     1.3 @@ -535,8 +535,21 @@
     1.4  lemma le_iff_diff_le_0: "a \<le> b \<longleftrightarrow> a - b \<le> 0"
     1.5    by (simp add: compare_rls)
     1.6  
     1.7 +lemmas group_simps =
     1.8 +  add_ac
     1.9 +  add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2
    1.10 +  diff_eq_eq eq_diff_eq diff_minus [symmetric] uminus_add_conv_diff
    1.11 +  diff_less_eq less_diff_eq diff_le_eq le_diff_eq
    1.12 +
    1.13  end
    1.14  
    1.15 +lemmas group_simps =
    1.16 +  mult_ac
    1.17 +  add_ac
    1.18 +  add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2
    1.19 +  diff_eq_eq eq_diff_eq diff_minus [symmetric] uminus_add_conv_diff
    1.20 +  diff_less_eq less_diff_eq diff_le_eq le_diff_eq
    1.21 +
    1.22  class ordered_ab_semigroup_add =
    1.23    linorder + pordered_ab_semigroup_add
    1.24  
    1.25 @@ -565,6 +578,12 @@
    1.26    qed
    1.27  qed
    1.28  
    1.29 +class ordered_ab_group_add =
    1.30 +  linorder + pordered_ab_group_add
    1.31 +
    1.32 +subclass (in ordered_ab_group_add) ordered_cancel_ab_semigroup_add 
    1.33 +  by unfold_locales
    1.34 +
    1.35  -- {* FIXME localize the following *}
    1.36  
    1.37  lemma add_increasing:
    1.38 @@ -752,6 +771,12 @@
    1.39      (simp add: le_infI)
    1.40  qed
    1.41  
    1.42 +lemma neg_inf_eq_sup: "- inf a b = sup (-a) (-b)"
    1.43 +  by (simp add: inf_eq_neg_sup)
    1.44 +
    1.45 +lemma neg_sup_eq_inf: "- sup a b = inf (-a) (-b)"
    1.46 +  by (simp add: sup_eq_neg_inf)
    1.47 +
    1.48  lemma add_eq_inf_sup: "a + b = sup a b + inf a b"
    1.49  proof -
    1.50    have "0 = - inf 0 (a-b) + inf (a-b) 0" by (simp add: inf_commute)
    1.51 @@ -776,6 +801,21 @@
    1.52    pprt :: "'a \<Rightarrow> 'a" where
    1.53    "pprt x = sup x 0"
    1.54  
    1.55 +lemma pprt_neg: "pprt (- x) = - nprt x"
    1.56 +proof -
    1.57 +  have "sup (- x) 0 = sup (- x) (- 0)" unfolding minus_zero ..
    1.58 +  also have "\<dots> = - inf x 0" unfolding neg_inf_eq_sup ..
    1.59 +  finally have "sup (- x) 0 = - inf x 0" .
    1.60 +  then show ?thesis unfolding pprt_def nprt_def .
    1.61 +qed
    1.62 +
    1.63 +lemma nprt_neg: "nprt (- x) = - pprt x"
    1.64 +proof -
    1.65 +  from pprt_neg have "pprt (- (- x)) = - nprt (- x)" .
    1.66 +  then have "pprt x = - nprt (- x)" by simp
    1.67 +  then show ?thesis by simp
    1.68 +qed
    1.69 +
    1.70  lemma prts: "a = pprt a + nprt a"
    1.71    by (simp add: pprt_def nprt_def add_eq_inf_sup[symmetric])
    1.72  
    1.73 @@ -904,38 +944,67 @@
    1.74    ultimately show ?thesis by blast
    1.75  qed
    1.76  
    1.77 +declare neg_inf_eq_sup [simp] neg_sup_eq_inf [simp]
    1.78 +
    1.79 +lemma le_minus_self_iff: "a \<le> - a \<longleftrightarrow> a \<le> 0"
    1.80 +proof -
    1.81 +  from add_le_cancel_left [of "uminus a" "plus a a" zero]
    1.82 +  have "(a <= -a) = (a+a <= 0)" 
    1.83 +    by (simp add: add_assoc[symmetric])
    1.84 +  thus ?thesis by simp
    1.85 +qed
    1.86 +
    1.87 +lemma minus_le_self_iff: "- a \<le> a \<longleftrightarrow> 0 \<le> a"
    1.88 +proof -
    1.89 +  from add_le_cancel_left [of "uminus a" zero "plus a a"]
    1.90 +  have "(-a <= a) = (0 <= a+a)" 
    1.91 +    by (simp add: add_assoc[symmetric])
    1.92 +  thus ?thesis by simp
    1.93 +qed
    1.94 +
    1.95 +lemma zero_le_iff_zero_nprt: "0 \<le> a \<longleftrightarrow> nprt a = 0"
    1.96 +  by (simp add: le_iff_inf nprt_def inf_commute)
    1.97 +
    1.98 +lemma le_zero_iff_zero_pprt: "a \<le> 0 \<longleftrightarrow> pprt a = 0"
    1.99 +  by (simp add: le_iff_sup pprt_def sup_commute)
   1.100 +
   1.101 +lemma le_zero_iff_pprt_id: "0 \<le> a \<longleftrightarrow> pprt a = a"
   1.102 +  by (simp add: le_iff_sup pprt_def sup_commute)
   1.103 +
   1.104 +lemma zero_le_iff_nprt_id: "a \<le> 0 \<longleftrightarrow> nprt a = a"
   1.105 +  by (simp add: le_iff_inf nprt_def inf_commute)
   1.106 +
   1.107 +lemma pprt_mono [simp, noatp]: "a \<le> b \<Longrightarrow> pprt a \<le> pprt b"
   1.108 +  by (simp add: le_iff_sup pprt_def sup_ACI sup_assoc [symmetric, of a])
   1.109 +
   1.110 +lemma nprt_mono [simp, noatp]: "a \<le> b \<Longrightarrow> nprt a \<le> nprt b"
   1.111 +  by (simp add: le_iff_inf nprt_def inf_ACI inf_assoc [symmetric, of a])
   1.112 +
   1.113  end
   1.114  
   1.115  lemmas add_sup_inf_distribs = add_inf_distrib_right add_inf_distrib_left add_sup_distrib_right add_sup_distrib_left
   1.116  
   1.117 -class lordered_ab_group_abs = lordered_ab_group + abs +
   1.118 -  assumes abs_lattice: "\<bar>x\<bar> = sup x (- x)"
   1.119 +
   1.120 +class pordered_ab_group_add_abs = pordered_ab_group_add + abs +
   1.121 +  assumes abs_ge_zero [simp]: "\<bar>a\<bar> \<ge> 0"
   1.122 +    and abs_ge_self: "a \<le> \<bar>a\<bar>"
   1.123 +    and abs_of_nonneg [simp]: "0 \<le> a \<Longrightarrow> \<bar>a\<bar> = a"
   1.124 +    and abs_leI: "a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b"
   1.125 +    and abs_eq_0 [simp]: "\<bar>a\<bar> = 0 \<longleftrightarrow> a = 0"
   1.126 +    and abs_minus_cancel [simp]: "\<bar>-a\<bar> = \<bar>a\<bar>"
   1.127 +    and abs_idempotent [simp]: "\<bar>\<bar>a\<bar>\<bar> = \<bar>a\<bar>"
   1.128 +    and abs_triangle_ineq: "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
   1.129  begin
   1.130  
   1.131  lemma abs_zero [simp]: "\<bar>0\<bar> = 0"
   1.132 -  by (simp add: abs_lattice)
   1.133 -
   1.134 -lemma abs_eq_0 [simp]: "\<bar>a\<bar> = 0 \<longleftrightarrow> a = 0"
   1.135 -  by (simp add: abs_lattice)
   1.136 +  by simp
   1.137  
   1.138  lemma abs_0_eq [simp, noatp]: "0 = \<bar>a\<bar> \<longleftrightarrow> a = 0"
   1.139  proof -
   1.140 -  have "(0 = abs a) = (abs a = 0)" by (simp only: eq_ac)
   1.141 +  have "0 = \<bar>a\<bar> \<longleftrightarrow> \<bar>a\<bar> = 0" by (simp only: eq_ac)
   1.142    thus ?thesis by simp
   1.143  qed
   1.144  
   1.145 -lemma neg_inf_eq_sup [simp]: "- inf a b = sup (-a) (-b)"
   1.146 -  by (simp add: inf_eq_neg_sup)
   1.147 -
   1.148 -lemma neg_sup_eq_inf [simp]: "- sup a b = inf (-a) (-b)"
   1.149 -  by (simp del: neg_inf_eq_sup add: sup_eq_neg_inf)
   1.150 -
   1.151 -lemma abs_ge_zero [simp]: "0 \<le> \<bar>a\<bar>"
   1.152 -proof -
   1.153 -  have a: "a \<le> \<bar>a\<bar>" and b: "- a \<le> \<bar>a\<bar>" by (auto simp add: abs_lattice)
   1.154 -  show ?thesis by (rule add_mono [OF a b, simplified])
   1.155 -qed
   1.156 -  
   1.157  lemma abs_le_zero_iff [simp]: "\<bar>a\<bar> \<le> 0 \<longleftrightarrow> a = 0" 
   1.158  proof
   1.159    assume "\<bar>a\<bar> \<le> 0"
   1.160 @@ -955,20 +1024,11 @@
   1.161    show ?thesis by (simp add: a)
   1.162  qed
   1.163  
   1.164 -lemma abs_ge_self: "a \<le> \<bar>a\<bar>"
   1.165 -  by (auto simp add: abs_lattice)
   1.166 -
   1.167  lemma abs_ge_minus_self: "- a \<le> \<bar>a\<bar>"
   1.168 -  by (auto simp add: abs_lattice)
   1.169 -
   1.170 -lemma abs_minus_cancel [simp]: "\<bar>-a\<bar> = \<bar>a\<bar>"
   1.171 -  by (simp add: abs_lattice sup_commute)
   1.172 -
   1.173 -lemma abs_idempotent [simp]: "\<bar>\<bar>a\<bar>\<bar> = \<bar>a\<bar>"
   1.174 -apply (simp add: abs_lattice [of "abs a"])
   1.175 -apply (subst sup_absorb1)
   1.176 -apply (rule order_trans [of _ zero])
   1.177 -by auto
   1.178 +proof -
   1.179 +  have "- a \<le> \<bar>-a\<bar>" by (rule abs_ge_self)
   1.180 +  then show ?thesis by simp
   1.181 +qed
   1.182  
   1.183  lemma abs_minus_commute: 
   1.184    "\<bar>a - b\<bar> = \<bar>b - a\<bar>"
   1.185 @@ -978,73 +1038,24 @@
   1.186    finally show ?thesis .
   1.187  qed
   1.188  
   1.189 -lemma abs_prts: "\<bar>a\<bar> = pprt a - nprt a"
   1.190 +lemma abs_of_pos: "0 < a \<Longrightarrow> \<bar>a\<bar> = a"
   1.191 +  by (rule abs_of_nonneg, rule less_imp_le)
   1.192 +
   1.193 +lemma abs_of_nonpos [simp]:
   1.194 +  assumes "a \<le> 0"
   1.195 +  shows "\<bar>a\<bar> = - a"
   1.196  proof -
   1.197 -  have "0 \<le> \<bar>a\<bar>" by simp
   1.198 -  then have "0 \<le> sup a (- a)" unfolding abs_lattice .
   1.199 -  then have "sup (sup a (- a)) 0 = sup a (- a)" by (rule sup_absorb1)
   1.200 -  then show ?thesis
   1.201 -    by (simp add: add_sup_inf_distribs sup_ACI
   1.202 -      pprt_def nprt_def diff_minus abs_lattice)
   1.203 +  let ?b = "- a"
   1.204 +  have "- ?b \<le> 0 \<Longrightarrow> \<bar>- ?b\<bar> = - (- ?b)"
   1.205 +  unfolding abs_minus_cancel [of "?b"]
   1.206 +  unfolding neg_le_0_iff_le [of "?b"]
   1.207 +  unfolding minus_minus by (erule abs_of_nonneg)
   1.208 +  then show ?thesis using assms by auto
   1.209  qed
   1.210    
   1.211 -lemma zero_le_iff_zero_nprt: "0 \<le> a \<longleftrightarrow> nprt a = 0"
   1.212 -  by (simp add: le_iff_inf nprt_def inf_commute)
   1.213 -
   1.214 -lemma le_zero_iff_zero_pprt: "a \<le> 0 \<longleftrightarrow> pprt a = 0"
   1.215 -  by (simp add: le_iff_sup pprt_def sup_commute)
   1.216 -
   1.217 -lemma le_zero_iff_pprt_id: "0 \<le> a \<longleftrightarrow> pprt a = a"
   1.218 -  by (simp add: le_iff_sup pprt_def sup_commute)
   1.219 -
   1.220 -lemma zero_le_iff_nprt_id: "a \<le> 0 \<longleftrightarrow> nprt a = a"
   1.221 -by (simp add: le_iff_inf nprt_def inf_commute)
   1.222 -
   1.223 -lemma pprt_mono [simp, noatp]: "a \<le> b \<Longrightarrow> pprt a \<le> pprt b"
   1.224 -  by (simp add: le_iff_sup pprt_def sup_ACI sup_assoc [symmetric, of a])
   1.225 -
   1.226 -lemma nprt_mono [simp, noatp]: "a \<le> b \<Longrightarrow> nprt a \<le> nprt b"
   1.227 -  by (simp add: le_iff_inf nprt_def inf_ACI inf_assoc [symmetric, of a])
   1.228 -
   1.229 -lemma pprt_neg: "pprt (- x) = - nprt x"
   1.230 -  by (simp add: pprt_def nprt_def)
   1.231 -
   1.232 -lemma nprt_neg: "nprt (- x) = - pprt x"
   1.233 -  by (simp add: pprt_def nprt_def)
   1.234 -
   1.235 -lemma abs_of_nonneg [simp]: "0 \<le> a \<Longrightarrow> \<bar>a\<bar> = a"
   1.236 -  by (simp add: iffD1 [OF zero_le_iff_zero_nprt]
   1.237 -    iffD1[OF le_zero_iff_pprt_id] abs_prts)
   1.238 -
   1.239 -lemma abs_of_pos: "0 < x \<Longrightarrow> \<bar>x\<bar> = x"
   1.240 -  by (rule abs_of_nonneg, rule less_imp_le)
   1.241 -
   1.242 -lemma abs_of_nonpos [simp]: "a \<le> 0 \<Longrightarrow> \<bar>a\<bar> = - a"
   1.243 -  by (simp add: iffD1 [OF le_zero_iff_zero_pprt]
   1.244 -    iffD1 [OF zero_le_iff_nprt_id] abs_prts)
   1.245 -
   1.246 -lemma abs_of_neg: "x < 0 \<Longrightarrow> \<bar>x\<bar> = - x"
   1.247 +lemma abs_of_neg: "a < 0 \<Longrightarrow> \<bar>a\<bar> = - a"
   1.248    by (rule abs_of_nonpos, rule less_imp_le)
   1.249  
   1.250 -lemma abs_leI: "a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b"
   1.251 -  by (simp add: abs_lattice le_supI)
   1.252 -
   1.253 -lemma le_minus_self_iff: "a \<le> - a \<longleftrightarrow> a \<le> 0"
   1.254 -proof -
   1.255 -  from add_le_cancel_left [of "uminus a" "plus a a" zero]
   1.256 -  have "(a <= -a) = (a+a <= 0)" 
   1.257 -    by (simp add: add_assoc[symmetric])
   1.258 -  thus ?thesis by simp
   1.259 -qed
   1.260 -
   1.261 -lemma minus_le_self_iff: "- a \<le> a \<longleftrightarrow> 0 \<le> a"
   1.262 -proof -
   1.263 -  from add_le_cancel_left [of "uminus a" zero "plus a a"]
   1.264 -  have "(-a <= a) = (0 <= a+a)" 
   1.265 -    by (simp add: add_assoc[symmetric])
   1.266 -  thus ?thesis by simp
   1.267 -qed
   1.268 -
   1.269  lemma abs_le_D1: "\<bar>a\<bar> \<le> b \<Longrightarrow> a \<le> b"
   1.270    by (insert abs_ge_self, blast intro: order_trans)
   1.271  
   1.272 @@ -1054,20 +1065,6 @@
   1.273  lemma abs_le_iff: "\<bar>a\<bar> \<le> b \<longleftrightarrow> a \<le> b \<and> - a \<le> b"
   1.274    by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2)
   1.275  
   1.276 -lemma abs_triangle_ineq: "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
   1.277 -proof -
   1.278 -  have g:"abs a + abs b = sup (a+b) (sup (-a-b) (sup (-a+b) (a + (-b))))" (is "_=sup ?m ?n")
   1.279 -    by (simp add: abs_lattice add_sup_inf_distribs sup_ACI diff_minus)
   1.280 -  have a:"a+b <= sup ?m ?n" by (simp)
   1.281 -  have b:"-a-b <= ?n" by (simp) 
   1.282 -  have c:"?n <= sup ?m ?n" by (simp)
   1.283 -  from b c have d: "-a-b <= sup ?m ?n" by(rule order_trans)
   1.284 -  have e:"-a-b = -(a+b)" by (simp add: diff_minus)
   1.285 -  from a d e have "abs(a+b) <= sup ?m ?n" 
   1.286 -    by (drule_tac abs_leI, auto)
   1.287 -  with g[symmetric] show ?thesis by simp
   1.288 -qed
   1.289 -
   1.290  lemma abs_triangle_ineq2: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>a - b\<bar>"
   1.291    apply (simp add: compare_rls)
   1.292    apply (subgoal_tac "abs a = abs (plus (minus a b) b)")
   1.293 @@ -1102,7 +1099,7 @@
   1.294    finally show ?thesis .
   1.295  qed
   1.296  
   1.297 -lemma abs_add_abs[simp]:
   1.298 +lemma abs_add_abs [simp]:
   1.299    "\<bar>\<bar>a\<bar> + \<bar>b\<bar>\<bar> = \<bar>a\<bar> + \<bar>b\<bar>" (is "?L = ?R")
   1.300  proof (rule antisym)
   1.301    show "?L \<ge> ?R" by(rule abs_ge_self)
   1.302 @@ -1114,6 +1111,87 @@
   1.303  
   1.304  end
   1.305  
   1.306 +
   1.307 +class lordered_ab_group_abs = lordered_ab_group + abs +
   1.308 +  assumes abs_lattice: "\<bar>a\<bar> = sup a (- a)"
   1.309 +begin
   1.310 +
   1.311 +lemma abs_prts: "\<bar>a\<bar> = pprt a - nprt a"
   1.312 +proof -
   1.313 +  have "0 \<le> \<bar>a\<bar>"
   1.314 +  proof -
   1.315 +    have a: "a \<le> \<bar>a\<bar>" and b: "- a \<le> \<bar>a\<bar>" by (auto simp add: abs_lattice)
   1.316 +    show ?thesis by (rule add_mono [OF a b, simplified])
   1.317 +  qed
   1.318 +  then have "0 \<le> sup a (- a)" unfolding abs_lattice .
   1.319 +  then have "sup (sup a (- a)) 0 = sup a (- a)" by (rule sup_absorb1)
   1.320 +  then show ?thesis
   1.321 +    by (simp add: add_sup_inf_distribs sup_ACI
   1.322 +      pprt_def nprt_def diff_minus abs_lattice)
   1.323 +qed
   1.324 +
   1.325 +subclass pordered_ab_group_add_abs
   1.326 +proof -
   1.327 +  have abs_ge_zero [simp]: "\<And>a. 0 \<le> \<bar>a\<bar>"
   1.328 +  proof -
   1.329 +    fix a b
   1.330 +    have a: "a \<le> \<bar>a\<bar>" and b: "- a \<le> \<bar>a\<bar>" by (auto simp add: abs_lattice)
   1.331 +    show "0 \<le> \<bar>a\<bar>" by (rule add_mono [OF a b, simplified])
   1.332 +  qed
   1.333 +  have abs_leI: "\<And>a b. a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b"
   1.334 +    by (simp add: abs_lattice le_supI)
   1.335 +  show ?thesis
   1.336 +  proof unfold_locales
   1.337 +    fix a
   1.338 +    show "0 \<le> \<bar>a\<bar>" by simp
   1.339 +  next
   1.340 +    fix a
   1.341 +    show "a \<le> \<bar>a\<bar>"
   1.342 +      by (auto simp add: abs_lattice)
   1.343 +  next
   1.344 +    fix a
   1.345 +    show "\<bar>a\<bar> = 0 \<longleftrightarrow> a = 0"
   1.346 +      by (simp add: abs_lattice)
   1.347 +  next
   1.348 +    fix a
   1.349 +    show "\<bar>-a\<bar> = \<bar>a\<bar>"
   1.350 +      by (simp add: abs_lattice sup_commute)
   1.351 +  next
   1.352 +    fix a
   1.353 +    show "\<bar>\<bar>a\<bar>\<bar> = \<bar>a\<bar>"
   1.354 +    apply (simp add: abs_lattice [of "abs a"])
   1.355 +    apply (subst sup_absorb1)
   1.356 +    apply (rule order_trans [of _ zero])
   1.357 +    apply auto
   1.358 +    done
   1.359 +  next
   1.360 +    fix a
   1.361 +    show "0 \<le> a \<Longrightarrow> \<bar>a\<bar> = a"
   1.362 +      by (simp add: iffD1 [OF zero_le_iff_zero_nprt]
   1.363 +        iffD1[OF le_zero_iff_pprt_id] abs_prts)
   1.364 +  next
   1.365 +    fix a b
   1.366 +    show "a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b" by (erule abs_leI)
   1.367 +  next
   1.368 +    fix a b
   1.369 +    show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
   1.370 +    proof -
   1.371 +      have g:"abs a + abs b = sup (a+b) (sup (-a-b) (sup (-a+b) (a + (-b))))" (is "_=sup ?m ?n")
   1.372 +        by (simp add: abs_lattice add_sup_inf_distribs sup_ACI diff_minus)
   1.373 +      have a:"a+b <= sup ?m ?n" by (simp)
   1.374 +      have b:"-a-b <= ?n" by (simp) 
   1.375 +      have c:"?n <= sup ?m ?n" by (simp)
   1.376 +      from b c have d: "-a-b <= sup ?m ?n" by(rule order_trans)
   1.377 +      have e:"-a-b = -(a+b)" by (simp add: diff_minus)
   1.378 +      from a d e have "abs(a+b) <= sup ?m ?n" 
   1.379 +        by (drule_tac abs_leI, auto)
   1.380 +      with g[symmetric] show ?thesis by simp
   1.381 +    qed
   1.382 +  qed auto
   1.383 +qed
   1.384 +
   1.385 +end
   1.386 +
   1.387  lemma sup_eq_if:
   1.388    fixes a :: "'a\<Colon>{lordered_ab_group, linorder}"
   1.389    shows "sup a (- a) = (if a < 0 then - a else a)"
   1.390 @@ -1168,13 +1246,6 @@
   1.391    apply (simp_all add: prems)
   1.392    done
   1.393  
   1.394 -lemmas group_simps =
   1.395 -  mult_ac
   1.396 -  add_ac
   1.397 -  add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2
   1.398 -  diff_eq_eq eq_diff_eq diff_minus [symmetric] uminus_add_conv_diff
   1.399 -  diff_less_eq less_diff_eq diff_le_eq le_diff_eq
   1.400 -
   1.401  lemma estimate_by_abs:
   1.402    "a + b <= (c::'a::lordered_ab_group_abs) \<Longrightarrow> a <= c + abs b" 
   1.403  proof -