src/HOL/OrderedGroup.thy
changeset 23389 aaca6a8e5414
parent 23181 f52b555f8141
child 23477 f4b83f03cac9
     1.1 --- a/src/HOL/OrderedGroup.thy	Thu Jun 14 18:33:29 2007 +0200
     1.2 +++ b/src/HOL/OrderedGroup.thy	Thu Jun 14 18:33:31 2007 +0200
     1.3 @@ -377,10 +377,10 @@
     1.4  subsection {* Ordering Rules for Unary Minus *}
     1.5  
     1.6  lemma le_imp_neg_le:
     1.7 -      assumes "a \<le> (b::'a::{pordered_ab_semigroup_add_imp_le, ab_group_add})" shows "-b \<le> -a"
     1.8 +  assumes "a \<le> (b::'a::{pordered_ab_semigroup_add_imp_le, ab_group_add})" shows "-b \<le> -a"
     1.9  proof -
    1.10    have "-a+a \<le> -a+b"
    1.11 -    by (rule add_left_mono) 
    1.12 +    using `a \<le> b` by (rule add_left_mono) 
    1.13    hence "0 \<le> -a+b"
    1.14      by simp
    1.15    hence "0 + (-b) \<le> (-a + b) + (-b)"