diff r 1e29e2666a15 r e7e54a0b9197 src/HOL/Real.thy
 a/src/HOL/Real.thy Sat Nov 11 18:33:35 2017 +0000
+++ b/src/HOL/Real.thy Sat Nov 11 18:41:08 2017 +0000
@@ 1245,7 +1245,7 @@
lemma Rats_abs_nat_div_natE:
assumes "x \ \"
 obtains m n :: nat where "n \ 0" and "\x\ = real m / real n" and "gcd m n = 1"
+ obtains m n :: nat where "n \ 0" and "\x\ = real m / real n" and "coprime m n"
proof 
from \x \ \\ obtain i :: int and n :: nat where "n \ 0" and "x = real_of_int i / real n"
by (auto simp add: Rats_eq_int_div_nat)
@@ 1281,6 +1281,8 @@
with gcd_k gcd_l have "?gcd * ?gcd' = ?gcd" by simp
with gcd show ?thesis by auto
qed
+ then have "coprime ?k ?l"
+ by (simp only: coprime_iff_gcd_eq_1)
ultimately show ?thesis ..
qed
@@ 1415,8 +1417,6 @@
for m :: nat
by (metis not_le real_of_nat_less_numeral_iff)
declare of_int_floor_le [simp] (* FIXME duplicate!? *)

lemma of_int_floor_cancel [simp]: "of_int \x\ = x \ (\n::int. x = of_int n)"
by (metis floor_of_int)
@@ 1424,7 +1424,7 @@
by linarith
lemma floor_eq2: "real_of_int n \ x \ x < real_of_int n + 1 \ \x\ = n"
 by linarith
+ by (fact floor_unique)
lemma floor_eq3: "real n < x \ x < real (Suc n) \ nat \x\ = n"
by linarith