src/HOL/Rat.thy

 *)
 
 section \<open>Rational numbers\<close>
 
 theory Rat
-  imports GCD Archimedean_Field
+  imports Archimedean_Field
 begin
 
 subsection \<open>Rational numbers as quotient\<close>
 
 subsubsection \<open>Construction of the type of rational numbers\<close>

 lemma quotient_of_denom_pos: "quotient_of r = (p, q) \<Longrightarrow> q > 0"
   by (cases r) (simp add: quotient_of_Fract normalize_denom_pos)
 
 lemma quotient_of_denom_pos': "snd (quotient_of r) > 0"
   using quotient_of_denom_pos [of r] by (simp add: prod_eq_iff)
-    
+
 lemma quotient_of_coprime: "quotient_of r = (p, q) \<Longrightarrow> coprime p q"
   by (cases r) (simp add: quotient_of_Fract normalize_coprime)
 
 lemma quotient_of_inject:
   assumes "quotient_of a = quotient_of b"