[STATEMENT]
lemma add_rel_frac:
  assumes "(r,s) \<in> R \<times> S" "(r',s')\<in> R \<times> S"
  shows "add_rel (r/s) (r'/s') = (r\<cdot>s' + r'\<cdot>s) / (s\<cdot>s')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. add_rel (r / s) (r' / s') = (r \<cdot> s' + r' \<cdot> s) / (s \<cdot> s')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. add_rel (r / s) (r' / s') = (r \<cdot> s' + r' \<cdot> s) / (s \<cdot> s')
[PROOF STEP]
define x where "x=(SOME x. x\<in>(r/s))"
[PROOF STATE]
proof (state)
this:
x = (SOME x. x \<in> r / s)

goal (1 subgoal):
 1. add_rel (r / s) (r' / s') = (r \<cdot> s' + r' \<cdot> s) / (s \<cdot> s')
[PROOF STEP]
define y where "y=(SOME y. y\<in>(r'/s'))"
[PROOF STATE]
proof (state)
this:
y = (SOME y. y \<in> r' / s')

goal (1 subgoal):
 1. add_rel (r / s) (r' / s') = (r \<cdot> s' + r' \<cdot> s) / (s \<cdot> s')
[PROOF STEP]
obtain s1 where [simp]:"s1 \<in> S" and x_eq:"s1 \<cdot> s \<cdot> fst x = s1 \<cdot> snd x \<cdot> r" and x_RS:"x \<in> R \<times> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s1. \<lbrakk>s1 \<in> S; s1 \<cdot> s \<cdot> fst x = s1 \<cdot> snd x \<cdot> r; x \<in> R \<times> S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using frac_eq_obtains[OF \<open>(r,s) \<in> R \<times> S\<close> x_def]
[PROOF STATE]
proof (prove)
using this:
(\<And>s1. \<lbrakk>s1 \<in> S; s1 \<cdot> s \<cdot> fst x = s1 \<cdot> snd x \<cdot> r; x \<in> R \<times> S\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>s1. \<lbrakk>s1 \<in> S; s1 \<cdot> s \<cdot> fst x = s1 \<cdot> snd x \<cdot> r; x \<in> R \<times> S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s1 \<in> S
s1 \<cdot> s \<cdot> fst x = s1 \<cdot> snd x \<cdot> r
x \<in> R \<times> S

goal (1 subgoal):
 1. add_rel (r / s) (r' / s') = (r \<cdot> s' + r' \<cdot> s) / (s \<cdot> s')
[PROOF STEP]
obtain s2 where [simp]:"s2 \<in> S" and y_eq:"s2 \<cdot> s' \<cdot> fst y = s2 \<cdot> snd y \<cdot> r'" and y_RS:"y \<in> R \<times> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s2. \<lbrakk>s2 \<in> S; s2 \<cdot> s' \<cdot> fst y = s2 \<cdot> snd y \<cdot> r'; y \<in> R \<times> S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using frac_eq_obtains[OF \<open>(r',s') \<in> R \<times> S\<close> y_def]
[PROOF STATE]
proof (prove)
using this:
(\<And>s1. \<lbrakk>s1 \<in> S; s1 \<cdot> s' \<cdot> fst y = s1 \<cdot> snd y \<cdot> r'; y \<in> R \<times> S\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>s2. \<lbrakk>s2 \<in> S; s2 \<cdot> s' \<cdot> fst y = s2 \<cdot> snd y \<cdot> r'; y \<in> R \<times> S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s2 \<in> S
s2 \<cdot> s' \<cdot> fst y = s2 \<cdot> snd y \<cdot> r'
y \<in> R \<times> S

goal (1 subgoal):
 1. add_rel (r / s) (r' / s') = (r \<cdot> s' + r' \<cdot> s) / (s \<cdot> s')
[PROOF STEP]
have "add_rel (r/s) (r'/s') = (fst x \<cdot> snd y + fst y \<cdot> snd x) / (snd x \<cdot> snd y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. add_rel (r / s) (r' / s') = (fst x \<cdot> snd y + fst y \<cdot> snd x) / (snd x \<cdot> snd y)
[PROOF STEP]
unfolding add_rel_def add_rel_aux_def x_def y_def Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (fst (SOME x. x \<in> r / s) \<cdot> snd (SOME y. y \<in> r' / s') + fst (SOME y. y \<in> r' / s') \<cdot> snd (SOME x. x \<in> r / s)) / (snd (SOME x. x \<in> r / s) \<cdot> snd (SOME y. y \<in> r' / s')) = (fst (SOME x. x \<in> r / s) \<cdot> snd (SOME y. y \<in> r' / s') + fst (SOME y. y \<in> r' / s') \<cdot> snd (SOME x. x \<in> r / s)) / (snd (SOME x. x \<in> r / s) \<cdot> snd (SOME y. y \<in> r' / s'))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
add_rel (r / s) (r' / s') = (fst x \<cdot> snd y + fst y \<cdot> snd x) / (snd x \<cdot> snd y)

goal (1 subgoal):
 1. add_rel (r / s) (r' / s') = (r \<cdot> s' + r' \<cdot> s) / (s \<cdot> s')
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
add_rel (r / s) (r' / s') = (fst x \<cdot> snd y + fst y \<cdot> snd x) / (snd x \<cdot> snd y)

goal (1 subgoal):
 1. add_rel (r / s) (r' / s') = (r \<cdot> s' + r' \<cdot> s) / (s \<cdot> s')
[PROOF STEP]
have "... = (r\<cdot>s' + r'\<cdot>s) / (s\<cdot>s')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (fst x \<cdot> snd y + fst y \<cdot> snd x) / (snd x \<cdot> snd y) = (r \<cdot> s' + r' \<cdot> s) / (s \<cdot> s')
[PROOF STEP]
proof (rule frac_eqI[of "s1 \<cdot> s2"])
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. s1 \<cdot> s2 \<in> S
 2. (fst x \<cdot> snd y + fst y \<cdot> snd x, snd x \<cdot> snd y) \<in> R \<times> S
 3. (r \<cdot> s' + r' \<cdot> s, s \<cdot> s') \<in> R \<times> S
 4. s1 \<cdot> s2 \<cdot> (s \<cdot> s') \<cdot> (fst x \<cdot> snd y + fst y \<cdot> snd x) = s1 \<cdot> s2 \<cdot> (snd x \<cdot> snd y) \<cdot> (r \<cdot> s' + r' \<cdot> s)
[PROOF STEP]
have "snd y \<cdot>  s' \<cdot> s2 \<cdot> (s1 \<cdot>  s \<cdot> fst x)  = snd y \<cdot> s' \<cdot> s2 \<cdot> (s1 \<cdot>  snd x \<cdot>  r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd y \<cdot> s' \<cdot> s2 \<cdot> (s1 \<cdot> s \<cdot> fst x) = snd y \<cdot> s' \<cdot> s2 \<cdot> (s1 \<cdot> snd x \<cdot> r)
[PROOF STEP]
using x_eq
[PROOF STATE]
proof (prove)
using this:
s1 \<cdot> s \<cdot> fst x = s1 \<cdot> snd x \<cdot> r

goal (1 subgoal):
 1. snd y \<cdot> s' \<cdot> s2 \<cdot> (s1 \<cdot> s \<cdot> fst x) = snd y \<cdot> s' \<cdot> s2 \<cdot> (s1 \<cdot> snd x \<cdot> r)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
snd y \<cdot> s' \<cdot> s2 \<cdot> (s1 \<cdot> s \<cdot> fst x) = snd y \<cdot> s' \<cdot> s2 \<cdot> (s1 \<cdot> snd x \<cdot> r)

goal (4 subgoals):
 1. s1 \<cdot> s2 \<in> S
 2. (fst x \<cdot> snd y + fst y \<cdot> snd x, snd x \<cdot> snd y) \<in> R \<times> S
 3. (r \<cdot> s' + r' \<cdot> s, s \<cdot> s') \<in> R \<times> S
 4. s1 \<cdot> s2 \<cdot> (s \<cdot> s') \<cdot> (fst x \<cdot> snd y + fst y \<cdot> snd x) = s1 \<cdot> s2 \<cdot> (snd x \<cdot> snd y) \<cdot> (r \<cdot> s' + r' \<cdot> s)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
snd y \<cdot> s' \<cdot> s2 \<cdot> (s1 \<cdot> s \<cdot> fst x) = snd y \<cdot> s' \<cdot> s2 \<cdot> (s1 \<cdot> snd x \<cdot> r)
[PROOF STEP]
have "s1 \<cdot> s2 \<cdot> s \<cdot> s' \<cdot> fst x \<cdot> snd y =  s1 \<cdot> s2 \<cdot> snd x \<cdot> snd y \<cdot> r \<cdot> s'"
[PROOF STATE]
proof (prove)
using this:
snd y \<cdot> s' \<cdot> s2 \<cdot> (s1 \<cdot> s \<cdot> fst x) = snd y \<cdot> s' \<cdot> s2 \<cdot> (s1 \<cdot> snd x \<cdot> r)

goal (1 subgoal):
 1. s1 \<cdot> s2 \<cdot> s \<cdot> s' \<cdot> fst x \<cdot> snd y = s1 \<cdot> s2 \<cdot> snd x \<cdot> snd y \<cdot> r \<cdot> s'
[PROOF STEP]
using comm.multiplicative.associative assms x_RS y_RS comm.comm_mult
[PROOF STATE]
proof (prove)
using this:
snd y \<cdot> s' \<cdot> s2 \<cdot> (s1 \<cdot> s \<cdot> fst x) = snd y \<cdot> s' \<cdot> s2 \<cdot> (s1 \<cdot> snd x \<cdot> r)
\<lbrakk>?a \<in> R; ?b \<in> R; ?c \<in> R\<rbrakk> \<Longrightarrow> ?a \<cdot> ?b \<cdot> ?c = ?a \<cdot> (?b \<cdot> ?c)
(r, s) \<in> R \<times> S
(r', s') \<in> R \<times> S
x \<in> R \<times> S
y \<in> R \<times> S
\<lbrakk>?a \<in> R; ?b \<in> R\<rbrakk> \<Longrightarrow> ?a \<cdot> ?b = ?b \<cdot> ?a

goal (1 subgoal):
 1. s1 \<cdot> s2 \<cdot> s \<cdot> s' \<cdot> fst x \<cdot> snd y = s1 \<cdot> s2 \<cdot> snd x \<cdot> snd y \<cdot> r \<cdot> s'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s1 \<cdot> s2 \<cdot> s \<cdot> s' \<cdot> fst x \<cdot> snd y = s1 \<cdot> s2 \<cdot> snd x \<cdot> snd y \<cdot> r \<cdot> s'

goal (4 subgoals):
 1. s1 \<cdot> s2 \<in> S
 2. (fst x \<cdot> snd y + fst y \<cdot> snd x, snd x \<cdot> snd y) \<in> R \<times> S
 3. (r \<cdot> s' + r' \<cdot> s, s \<cdot> s') \<in> R \<times> S
 4. s1 \<cdot> s2 \<cdot> (s \<cdot> s') \<cdot> (fst x \<cdot> snd y + fst y \<cdot> snd x) = s1 \<cdot> s2 \<cdot> (snd x \<cdot> snd y) \<cdot> (r \<cdot> s' + r' \<cdot> s)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
s1 \<cdot> s2 \<cdot> s \<cdot> s' \<cdot> fst x \<cdot> snd y = s1 \<cdot> s2 \<cdot> snd x \<cdot> snd y \<cdot> r \<cdot> s'

goal (4 subgoals):
 1. s1 \<cdot> s2 \<in> S
 2. (fst x \<cdot> snd y + fst y \<cdot> snd x, snd x \<cdot> snd y) \<in> R \<times> S
 3. (r \<cdot> s' + r' \<cdot> s, s \<cdot> s') \<in> R \<times> S
 4. s1 \<cdot> s2 \<cdot> (s \<cdot> s') \<cdot> (fst x \<cdot> snd y + fst y \<cdot> snd x) = s1 \<cdot> s2 \<cdot> (snd x \<cdot> snd y) \<cdot> (r \<cdot> s' + r' \<cdot> s)
[PROOF STEP]
have "snd x \<cdot> s \<cdot>s1 \<cdot> (s2 \<cdot> s' \<cdot> fst y) = snd x \<cdot> s \<cdot>s1 \<cdot> (s2 \<cdot> snd y \<cdot> r')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd x \<cdot> s \<cdot> s1 \<cdot> (s2 \<cdot> s' \<cdot> fst y) = snd x \<cdot> s \<cdot> s1 \<cdot> (s2 \<cdot> snd y \<cdot> r')
[PROOF STEP]
using y_eq
[PROOF STATE]
proof (prove)
using this:
s2 \<cdot> s' \<cdot> fst y = s2 \<cdot> snd y \<cdot> r'

goal (1 subgoal):
 1. snd x \<cdot> s \<cdot> s1 \<cdot> (s2 \<cdot> s' \<cdot> fst y) = snd x \<cdot> s \<cdot> s1 \<cdot> (s2 \<cdot> snd y \<cdot> r')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
snd x \<cdot> s \<cdot> s1 \<cdot> (s2 \<cdot> s' \<cdot> fst y) = snd x \<cdot> s \<cdot> s1 \<cdot> (s2 \<cdot> snd y \<cdot> r')

goal (4 subgoals):
 1. s1 \<cdot> s2 \<in> S
 2. (fst x \<cdot> snd y + fst y \<cdot> snd x, snd x \<cdot> snd y) \<in> R \<times> S
 3. (r \<cdot> s' + r' \<cdot> s, s \<cdot> s') \<in> R \<times> S
 4. s1 \<cdot> s2 \<cdot> (s \<cdot> s') \<cdot> (fst x \<cdot> snd y + fst y \<cdot> snd x) = s1 \<cdot> s2 \<cdot> (snd x \<cdot> snd y) \<cdot> (r \<cdot> s' + r' \<cdot> s)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
snd x \<cdot> s \<cdot> s1 \<cdot> (s2 \<cdot> s' \<cdot> fst y) = snd x \<cdot> s \<cdot> s1 \<cdot> (s2 \<cdot> snd y \<cdot> r')
[PROOF STEP]
have "s1 \<cdot> s2 \<cdot> s \<cdot> s' \<cdot> fst y \<cdot> snd x = s1 \<cdot> s2 \<cdot> snd x \<cdot> snd y \<cdot> r' \<cdot> s"
[PROOF STATE]
proof (prove)
using this:
snd x \<cdot> s \<cdot> s1 \<cdot> (s2 \<cdot> s' \<cdot> fst y) = snd x \<cdot> s \<cdot> s1 \<cdot> (s2 \<cdot> snd y \<cdot> r')

goal (1 subgoal):
 1. s1 \<cdot> s2 \<cdot> s \<cdot> s' \<cdot> fst y \<cdot> snd x = s1 \<cdot> s2 \<cdot> snd x \<cdot> snd y \<cdot> r' \<cdot> s
[PROOF STEP]
using comm.multiplicative.associative assms x_RS y_RS comm.comm_mult
[PROOF STATE]
proof (prove)
using this:
snd x \<cdot> s \<cdot> s1 \<cdot> (s2 \<cdot> s' \<cdot> fst y) = snd x \<cdot> s \<cdot> s1 \<cdot> (s2 \<cdot> snd y \<cdot> r')
\<lbrakk>?a \<in> R; ?b \<in> R; ?c \<in> R\<rbrakk> \<Longrightarrow> ?a \<cdot> ?b \<cdot> ?c = ?a \<cdot> (?b \<cdot> ?c)
(r, s) \<in> R \<times> S
(r', s') \<in> R \<times> S
x \<in> R \<times> S
y \<in> R \<times> S
\<lbrakk>?a \<in> R; ?b \<in> R\<rbrakk> \<Longrightarrow> ?a \<cdot> ?b = ?b \<cdot> ?a

goal (1 subgoal):
 1. s1 \<cdot> s2 \<cdot> s \<cdot> s' \<cdot> fst y \<cdot> snd x = s1 \<cdot> s2 \<cdot> snd x \<cdot> snd y \<cdot> r' \<cdot> s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s1 \<cdot> s2 \<cdot> s \<cdot> s' \<cdot> fst y \<cdot> snd x = s1 \<cdot> s2 \<cdot> snd x \<cdot> snd y \<cdot> r' \<cdot> s

goal (4 subgoals):
 1. s1 \<cdot> s2 \<in> S
 2. (fst x \<cdot> snd y + fst y \<cdot> snd x, snd x \<cdot> snd y) \<in> R \<times> S
 3. (r \<cdot> s' + r' \<cdot> s, s \<cdot> s') \<in> R \<times> S
 4. s1 \<cdot> s2 \<cdot> (s \<cdot> s') \<cdot> (fst x \<cdot> snd y + fst y \<cdot> snd x) = s1 \<cdot> s2 \<cdot> (snd x \<cdot> snd y) \<cdot> (r \<cdot> s' + r' \<cdot> s)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
s1 \<cdot> s2 \<cdot> s \<cdot> s' \<cdot> fst x \<cdot> snd y = s1 \<cdot> s2 \<cdot> snd x \<cdot> snd y \<cdot> r \<cdot> s'
s1 \<cdot> s2 \<cdot> s \<cdot> s' \<cdot> fst y \<cdot> snd x = s1 \<cdot> s2 \<cdot> snd x \<cdot> snd y \<cdot> r' \<cdot> s
[PROOF STEP]
show "s1 \<cdot> s2 \<cdot> (s \<cdot> s') \<cdot> (fst x \<cdot> snd y + fst y \<cdot> snd x)
        = s1 \<cdot> s2 \<cdot> (snd x \<cdot> snd y) \<cdot> (r \<cdot> s' + r' \<cdot> s)"
[PROOF STATE]
proof (prove)
using this:
s1 \<cdot> s2 \<cdot> s \<cdot> s' \<cdot> fst x \<cdot> snd y = s1 \<cdot> s2 \<cdot> snd x \<cdot> snd y \<cdot> r \<cdot> s'
s1 \<cdot> s2 \<cdot> s \<cdot> s' \<cdot> fst y \<cdot> snd x = s1 \<cdot> s2 \<cdot> snd x \<cdot> snd y \<cdot> r' \<cdot> s

goal (1 subgoal):
 1. s1 \<cdot> s2 \<cdot> (s \<cdot> s') \<cdot> (fst x \<cdot> snd y + fst y \<cdot> snd x) = s1 \<cdot> s2 \<cdot> (snd x \<cdot> snd y) \<cdot> (r \<cdot> s' + r' \<cdot> s)
[PROOF STEP]
using comm.multiplicative.associative assms x_RS y_RS comm.distributive
[PROOF STATE]
proof (prove)
using this:
s1 \<cdot> s2 \<cdot> s \<cdot> s' \<cdot> fst x \<cdot> snd y = s1 \<cdot> s2 \<cdot> snd x \<cdot> snd y \<cdot> r \<cdot> s'
s1 \<cdot> s2 \<cdot> s \<cdot> s' \<cdot> fst y \<cdot> snd x = s1 \<cdot> s2 \<cdot> snd x \<cdot> snd y \<cdot> r' \<cdot> s
\<lbrakk>?a \<in> R; ?b \<in> R; ?c \<in> R\<rbrakk> \<Longrightarrow> ?a \<cdot> ?b \<cdot> ?c = ?a \<cdot> (?b \<cdot> ?c)
(r, s) \<in> R \<times> S
(r', s') \<in> R \<times> S
x \<in> R \<times> S
y \<in> R \<times> S
\<lbrakk>?a \<in> R; ?b \<in> R; ?c \<in> R\<rbrakk> \<Longrightarrow> ?a \<cdot> (?b + ?c) = ?a \<cdot> ?b + ?a \<cdot> ?c
\<lbrakk>?a \<in> R; ?b \<in> R; ?c \<in> R\<rbrakk> \<Longrightarrow> (?b + ?c) \<cdot> ?a = ?b \<cdot> ?a + ?c \<cdot> ?a

goal (1 subgoal):
 1. s1 \<cdot> s2 \<cdot> (s \<cdot> s') \<cdot> (fst x \<cdot> snd y + fst y \<cdot> snd x) = s1 \<cdot> s2 \<cdot> (snd x \<cdot> snd y) \<cdot> (r \<cdot> s' + r' \<cdot> s)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s1 \<cdot> s2 \<cdot> (s \<cdot> s') \<cdot> (fst x \<cdot> snd y + fst y \<cdot> snd x) = s1 \<cdot> s2 \<cdot> (snd x \<cdot> snd y) \<cdot> (r \<cdot> s' + r' \<cdot> s)

goal (3 subgoals):
 1. s1 \<cdot> s2 \<in> S
 2. (fst x \<cdot> snd y + fst y \<cdot> snd x, snd x \<cdot> snd y) \<in> R \<times> S
 3. (r \<cdot> s' + r' \<cdot> s, s \<cdot> s') \<in> R \<times> S
[PROOF STEP]
show "s1 \<cdot> s2 \<in> S" "(fst x \<cdot> snd y + fst y \<cdot> snd x, snd x \<cdot> snd y) \<in> R \<times> S"
        "(r \<cdot> s' + r' \<cdot> s, s \<cdot> s') \<in> R \<times> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s1 \<cdot> s2 \<in> S &&& (fst x \<cdot> snd y + fst y \<cdot> snd x, snd x \<cdot> snd y) \<in> R \<times> S &&& (r \<cdot> s' + r' \<cdot> s, s \<cdot> s') \<in> R \<times> S
[PROOF STEP]
using assms x_RS y_RS
[PROOF STATE]
proof (prove)
using this:
(r, s) \<in> R \<times> S
(r', s') \<in> R \<times> S
x \<in> R \<times> S
y \<in> R \<times> S

goal (1 subgoal):
 1. s1 \<cdot> s2 \<in> S &&& (fst x \<cdot> snd y + fst y \<cdot> snd x, snd x \<cdot> snd y) \<in> R \<times> S &&& (r \<cdot> s' + r' \<cdot> s, s \<cdot> s') \<in> R \<times> S
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s1 \<cdot> s2 \<in> S
(fst x \<cdot> snd y + fst y \<cdot> snd x, snd x \<cdot> snd y) \<in> R \<times> S
(r \<cdot> s' + r' \<cdot> s, s \<cdot> s') \<in> R \<times> S

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(fst x \<cdot> snd y + fst y \<cdot> snd x) / (snd x \<cdot> snd y) = (r \<cdot> s' + r' \<cdot> s) / (s \<cdot> s')

goal (1 subgoal):
 1. add_rel (r / s) (r' / s') = (r \<cdot> s' + r' \<cdot> s) / (s \<cdot> s')
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
add_rel (r / s) (r' / s') = (r \<cdot> s' + r' \<cdot> s) / (s \<cdot> s')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
add_rel (r / s) (r' / s') = (r \<cdot> s' + r' \<cdot> s) / (s \<cdot> s')

goal (1 subgoal):
 1. add_rel (r / s) (r' / s') = (r \<cdot> s' + r' \<cdot> s) / (s \<cdot> s')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
add_rel (r / s) (r' / s') = (r \<cdot> s' + r' \<cdot> s) / (s \<cdot> s')

goal:
No subgoals!
[PROOF STEP]
qed