[STATEMENT]
lemma of_rat_less: "(of_rat r :: 'a::linordered_field) < of_rat s \<longleftrightarrow> r < s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (of_rat r < of_rat s) = (r < s)
[PROOF STEP]
proof (induct r, induct s)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>0 < b; 0 < ba\<rbrakk> \<Longrightarrow> (of_rat (Fract aa ba) < of_rat (Fract a b)) = (Fract aa ba < Fract a b)
[PROOF STEP]
fix a b c d :: int
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>0 < b; 0 < ba\<rbrakk> \<Longrightarrow> (of_rat (Fract aa ba) < of_rat (Fract a b)) = (Fract aa ba < Fract a b)
[PROOF STEP]
assume not_zero: "b > 0" "d > 0"
[PROOF STATE]
proof (state)
this:
0 < b
0 < d

goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>0 < b; 0 < ba\<rbrakk> \<Longrightarrow> (of_rat (Fract aa ba) < of_rat (Fract a b)) = (Fract aa ba < Fract a b)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < b
0 < d
[PROOF STEP]
have "b * d > 0"
[PROOF STATE]
proof (prove)
using this:
0 < b
0 < d

goal (1 subgoal):
 1. 0 < b * d
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < b * d

goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>0 < b; 0 < ba\<rbrakk> \<Longrightarrow> (of_rat (Fract aa ba) < of_rat (Fract a b)) = (Fract aa ba < Fract a b)
[PROOF STEP]
have of_int_divide_less_eq:
    "(of_int a :: 'a) / of_int b < of_int c / of_int d \<longleftrightarrow>
      (of_int a :: 'a) * of_int d < of_int c * of_int b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (of_int a / of_int b < of_int c / of_int d) = (of_int a * of_int d < of_int c * of_int b)
[PROOF STEP]
using not_zero
[PROOF STATE]
proof (prove)
using this:
0 < b
0 < d

goal (1 subgoal):
 1. (of_int a / of_int b < of_int c / of_int d) = (of_int a * of_int d < of_int c * of_int b)
[PROOF STEP]
by (simp add: pos_less_divide_eq pos_divide_less_eq)
[PROOF STATE]
proof (state)
this:
(of_int a / of_int b < of_int c / of_int d) = (of_int a * of_int d < of_int c * of_int b)

goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>0 < b; 0 < ba\<rbrakk> \<Longrightarrow> (of_rat (Fract aa ba) < of_rat (Fract a b)) = (Fract aa ba < Fract a b)
[PROOF STEP]
show "(of_rat (Fract a b) :: 'a::linordered_field) < of_rat (Fract c d) \<longleftrightarrow>
      Fract a b < Fract c d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (of_rat (Fract a b) < of_rat (Fract c d)) = (Fract a b < Fract c d)
[PROOF STEP]
using not_zero \<open>b * d > 0\<close>
[PROOF STATE]
proof (prove)
using this:
0 < b
0 < d
0 < b * d

goal (1 subgoal):
 1. (of_rat (Fract a b) < of_rat (Fract c d)) = (Fract a b < Fract c d)
[PROOF STEP]
by (simp add: of_rat_rat of_int_divide_less_eq of_int_mult [symmetric] del: of_int_mult)
[PROOF STATE]
proof (state)
this:
(of_rat (Fract a b) < of_rat (Fract c d)) = (Fract a b < Fract c d)

goal:
No subgoals!
[PROOF STEP]
qed