# HG changeset patch
# User paulson
# Date 1136973626 -3600
# Node ID bb99c2e705ca6a9058fa99e4199568b1f71ab944
# Parent  22f96cd085d51e9641d0899c4bbb420cda9e7fd8
tidied, and added missing thm divide_less_eq_1_neg

diff -r 22f96cd085d5 -r bb99c2e705ca src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Wed Jan 11 10:59:55 2006 +0100
+++ b/src/HOL/Ring_and_Field.thy	Wed Jan 11 11:00:26 2006 +0100
@@ -1647,47 +1647,52 @@
 
 lemma le_divide_eq_1_pos [simp]:
   fixes a :: "'a :: {ordered_field,division_by_zero}"
-  shows "0 < a \<Longrightarrow> (1 \<le> b / a) = (a \<le> b)"
+  shows "0 < a \<Longrightarrow> (1 \<le> b/a) = (a \<le> b)"
 by (auto simp add: le_divide_eq)
 
 lemma le_divide_eq_1_neg [simp]:
   fixes a :: "'a :: {ordered_field,division_by_zero}"
-  shows "a < 0 \<Longrightarrow> (1 \<le> b / a) = (b \<le> a)"
+  shows "a < 0 \<Longrightarrow> (1 \<le> b/a) = (b \<le> a)"
 by (auto simp add: le_divide_eq)
 
 lemma divide_le_eq_1_pos [simp]:
   fixes a :: "'a :: {ordered_field,division_by_zero}"
-  shows "0 < a \<Longrightarrow> (b / a \<le> 1) = (b \<le> a)"
+  shows "0 < a \<Longrightarrow> (b/a \<le> 1) = (b \<le> a)"
 by (auto simp add: divide_le_eq)
 
 lemma divide_le_eq_1_neg [simp]:
   fixes a :: "'a :: {ordered_field,division_by_zero}"
-  shows "a < 0 \<Longrightarrow> (b / a \<le> 1) = (a \<le> b)"
+  shows "a < 0 \<Longrightarrow> (b/a \<le> 1) = (a \<le> b)"
 by (auto simp add: divide_le_eq)
 
 lemma less_divide_eq_1_pos [simp]:
   fixes a :: "'a :: {ordered_field,division_by_zero}"
-  shows "0 < a \<Longrightarrow> (1 < b / a) = (a < b)"
+  shows "0 < a \<Longrightarrow> (1 < b/a) = (a < b)"
 by (auto simp add: less_divide_eq)
 
 lemma less_divide_eq_1_neg [simp]:
   fixes a :: "'a :: {ordered_field,division_by_zero}"
-  shows "a < 0 \<Longrightarrow> (1 < b / a) = (b < a)"
+  shows "a < 0 \<Longrightarrow> (1 < b/a) = (b < a)"
 by (auto simp add: less_divide_eq)
 
 lemma divide_less_eq_1_pos [simp]:
   fixes a :: "'a :: {ordered_field,division_by_zero}"
-  shows "0 < a \<Longrightarrow> (b / a < 1) = (b < a)"
+  shows "0 < a \<Longrightarrow> (b/a < 1) = (b < a)"
+by (auto simp add: divide_less_eq)
+
+lemma divide_less_eq_1_neg [simp]:
+  fixes a :: "'a :: {ordered_field,division_by_zero}"
+  shows "a < 0 \<Longrightarrow> b/a < 1 <-> a < b"
 by (auto simp add: divide_less_eq)
 
 lemma eq_divide_eq_1 [simp]:
   fixes a :: "'a :: {ordered_field,division_by_zero}"
-  shows "(1 = b / a) = ((a \<noteq> 0 & a = b))"
+  shows "(1 = b/a) = ((a \<noteq> 0 & a = b))"
 by (auto simp add: eq_divide_eq)
 
 lemma divide_eq_eq_1 [simp]:
   fixes a :: "'a :: {ordered_field,division_by_zero}"
-  shows "(b / a = 1) = ((a \<noteq> 0 & a = b))"
+  shows "(b/a = 1) = ((a \<noteq> 0 & a = b))"
 by (auto simp add: divide_eq_eq)
 
 subsection {* Reasoning about inequalities with division *}