--- a/src/HOL/Fields.thy Wed Apr 02 17:11:44 2014 +0200
+++ b/src/HOL/Fields.thy Wed Apr 02 16:34:37 2014 +0100
@@ -391,6 +391,9 @@
"(a / b) / c = a / (b * c)"
by (simp add: divide_inverse mult_assoc)
+lemma divide_divide_times_eq:
+ "(x / y) / (z / w) = (x * w) / (y * z)"
+ by simp
text {*Special Cancellation Simprules for Division*}
@@ -708,6 +711,14 @@
finally show ?thesis .
qed
+lemma frac_less_eq:
+ "y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> x / y < w / z \<longleftrightarrow> (x * z - w * y) / (y * z) < 0"
+ by (subst less_iff_diff_less_0) (simp add: diff_frac_eq )
+
+lemma frac_le_eq:
+ "y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> x / y \<le> w / z \<longleftrightarrow> (x * z - w * y) / (y * z) \<le> 0"
+ by (subst le_iff_diff_le_0) (simp add: diff_frac_eq )
+
text{* Lemmas @{text sign_simps} is a first attempt to automate proofs
of positivity/negativity needed for @{text field_simps}. Have not added @{text
sign_simps} to @{text field_simps} because the former can lead to case