# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1396452877 -3600
# Node ID 713f9b9a7e51fa46a5de698ddd2611dbde7fa083
# Parent  fbacdc80e1bce87e60c880254b45c81edccdec39
New theorems for extracting quotients

diff -r fbacdc80e1bc -r 713f9b9a7e51 src/HOL/Fields.thy
--- 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