[STATEMENT]
lemma surj_nat_to_rat_surj: "surj nat_to_rat_surj"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. surj nat_to_rat_surj
[PROOF STEP]
unfolding surj_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>y. \<exists>x. y = nat_to_rat_surj x
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. \<exists>x. y = nat_to_rat_surj x
[PROOF STEP]
fix r::rat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. \<exists>x. y = nat_to_rat_surj x
[PROOF STEP]
show "\<exists>n. r = nat_to_rat_surj n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n. r = nat_to_rat_surj n
[PROOF STEP]
proof (cases r)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>r = Fract a b; 0 < b; coprime a b\<rbrakk> \<Longrightarrow> \<exists>n. r = nat_to_rat_surj n
[PROOF STEP]
fix i j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>r = Fract a b; 0 < b; coprime a b\<rbrakk> \<Longrightarrow> \<exists>n. r = nat_to_rat_surj n
[PROOF STEP]
assume [simp]: "r = Fract i j" and "j > 0"
[PROOF STATE]
proof (state)
this:
r = Fract i j
0 < j

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>r = Fract a b; 0 < b; coprime a b\<rbrakk> \<Longrightarrow> \<exists>n. r = nat_to_rat_surj n
[PROOF STEP]
have "r = (let m = int_encode i; n = int_encode j in nat_to_rat_surj (prod_encode (m, n)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r = (let m = int_encode i; n = int_encode j in nat_to_rat_surj (prod_encode (m, n)))
[PROOF STEP]
by (simp add: Let_def nat_to_rat_surj_def)
[PROOF STATE]
proof (state)
this:
r = (let m = int_encode i; n = int_encode j in nat_to_rat_surj (prod_encode (m, n)))

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>r = Fract a b; 0 < b; coprime a b\<rbrakk> \<Longrightarrow> \<exists>n. r = nat_to_rat_surj n
[PROOF STEP]
thus "\<exists>n. r = nat_to_rat_surj n"
[PROOF STATE]
proof (prove)
using this:
r = (let m = int_encode i; n = int_encode j in nat_to_rat_surj (prod_encode (m, n)))

goal (1 subgoal):
 1. \<exists>n. r = nat_to_rat_surj n
[PROOF STEP]
by(auto simp: Let_def)
[PROOF STATE]
proof (state)
this:
\<exists>n. r = nat_to_rat_surj n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>n. r = nat_to_rat_surj n

goal:
No subgoals!
[PROOF STEP]
qed