add lemmas one_less_inverse and one_le_inverse
authorhuffman
Sat May 08 17:06:58 2010 -0700 (2010-05-08)
changeset 367749e444b09fbef
parent 36771 3e08b6789e66
child 36775 ba2a7096dd2b
add lemmas one_less_inverse and one_le_inverse
src/HOL/Fields.thy
     1.1 --- a/src/HOL/Fields.thy	Sat May 08 22:29:44 2010 +0200
     1.2 +++ b/src/HOL/Fields.thy	Sat May 08 17:06:58 2010 -0700
     1.3 @@ -397,6 +397,14 @@
     1.4    "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> inverse a \<le> inverse b \<longleftrightarrow> b \<le> a"
     1.5    by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg) 
     1.6  
     1.7 +lemma one_less_inverse:
     1.8 +  "0 < a \<Longrightarrow> a < 1 \<Longrightarrow> 1 < inverse a"
     1.9 +  using less_imp_inverse_less [of a 1, unfolded inverse_1] .
    1.10 +
    1.11 +lemma one_le_inverse:
    1.12 +  "0 < a \<Longrightarrow> a \<le> 1 \<Longrightarrow> 1 \<le> inverse a"
    1.13 +  using le_imp_inverse_le [of a 1, unfolded inverse_1] .
    1.14 +
    1.15  lemma pos_le_divide_eq [field_simps]: "0 < c ==> (a \<le> b/c) = (a*c \<le> b)"
    1.16  proof -
    1.17    assume less: "0<c"