# HG changeset patch
# User huffman
# Date 1273423141 25200
# Node ID ba2a7096dd2bf414b938f690e48287533378465e
# Parent  9e444b09fbef74992d1a5a661d0913832eb2a0b3# Parent  acb789f3936bf1849abb9f0ba6a1d80e2a6a5d88
merged

diff -r acb789f3936b -r ba2a7096dd2b src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Sun May 09 15:28:44 2010 +0200
+++ b/src/HOL/Fields.thy	Sun May 09 09:39:01 2010 -0700
@@ -397,6 +397,14 @@
   "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> inverse a \<le> inverse b \<longleftrightarrow> b \<le> a"
   by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg) 
 
+lemma one_less_inverse:
+  "0 < a \<Longrightarrow> a < 1 \<Longrightarrow> 1 < inverse a"
+  using less_imp_inverse_less [of a 1, unfolded inverse_1] .
+
+lemma one_le_inverse:
+  "0 < a \<Longrightarrow> a \<le> 1 \<Longrightarrow> 1 \<le> inverse a"
+  using le_imp_inverse_le [of a 1, unfolded inverse_1] .
+
 lemma pos_le_divide_eq [field_simps]: "0 < c ==> (a \<le> b/c) = (a*c \<le> b)"
 proof -
   assume less: "0<c"