[STATEMENT]
lemma cross_ratio_correct_cltn2:
  assumes "cross_ratio_correct p q r s"
  shows "cross_ratio_correct (apply_cltn2 p C) (apply_cltn2 q C)
  (apply_cltn2 r C) (apply_cltn2 s C)"
  (is "cross_ratio_correct ?pC ?qC ?rC ?sC")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cross_ratio_correct (apply_cltn2 p C) (apply_cltn2 q C) (apply_cltn2 r C) (apply_cltn2 s C)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cross_ratio_correct (apply_cltn2 p C) (apply_cltn2 q C) (apply_cltn2 r C) (apply_cltn2 s C)
[PROOF STEP]
from \<open>cross_ratio_correct p q r s\<close>
[PROOF STATE]
proof (chain)
picking this:
cross_ratio_correct p q r s
[PROOF STEP]
have "proj2_set_Col {p,q,r,s}"
    and "p \<noteq> q" and "r \<noteq> p" and "s \<noteq> p" and "r \<noteq> q"
[PROOF STATE]
proof (prove)
using this:
cross_ratio_correct p q r s

goal (1 subgoal):
 1. (proj2_set_Col {p, q, r, s} &&& p \<noteq> q) &&& r \<noteq> p &&& s \<noteq> p &&& r \<noteq> q
[PROOF STEP]
by (unfold cross_ratio_correct_def) simp_all
[PROOF STATE]
proof (state)
this:
proj2_set_Col {p, q, r, s}
p \<noteq> q
r \<noteq> p
s \<noteq> p
r \<noteq> q

goal (1 subgoal):
 1. cross_ratio_correct (apply_cltn2 p C) (apply_cltn2 q C) (apply_cltn2 r C) (apply_cltn2 s C)
[PROOF STEP]
have "{apply_cltn2 t C | t. t \<in> {p,q,r,s}} = {?pC,?qC,?rC,?sC}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {apply_cltn2 t C |t. t \<in> {p, q, r, s}} = {apply_cltn2 p C, apply_cltn2 q C, apply_cltn2 r C, apply_cltn2 s C}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{apply_cltn2 t C |t. t \<in> {p, q, r, s}} = {apply_cltn2 p C, apply_cltn2 q C, apply_cltn2 r C, apply_cltn2 s C}

goal (1 subgoal):
 1. cross_ratio_correct (apply_cltn2 p C) (apply_cltn2 q C) (apply_cltn2 r C) (apply_cltn2 s C)
[PROOF STEP]
with \<open>proj2_set_Col {p,q,r,s}\<close>
    and apply_cltn2_preserve_set_Col [of "{p,q,r,s}" C]
[PROOF STATE]
proof (chain)
picking this:
proj2_set_Col {p, q, r, s}
proj2_set_Col {p, q, r, s} \<Longrightarrow> proj2_set_Col {apply_cltn2 pa C |pa. pa \<in> {p, q, r, s}}
{apply_cltn2 t C |t. t \<in> {p, q, r, s}} = {apply_cltn2 p C, apply_cltn2 q C, apply_cltn2 r C, apply_cltn2 s C}
[PROOF STEP]
have "proj2_set_Col {?pC,?qC,?rC,?sC}"
[PROOF STATE]
proof (prove)
using this:
proj2_set_Col {p, q, r, s}
proj2_set_Col {p, q, r, s} \<Longrightarrow> proj2_set_Col {apply_cltn2 pa C |pa. pa \<in> {p, q, r, s}}
{apply_cltn2 t C |t. t \<in> {p, q, r, s}} = {apply_cltn2 p C, apply_cltn2 q C, apply_cltn2 r C, apply_cltn2 s C}

goal (1 subgoal):
 1. proj2_set_Col {apply_cltn2 p C, apply_cltn2 q C, apply_cltn2 r C, apply_cltn2 s C}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
proj2_set_Col {apply_cltn2 p C, apply_cltn2 q C, apply_cltn2 r C, apply_cltn2 s C}

goal (1 subgoal):
 1. cross_ratio_correct (apply_cltn2 p C) (apply_cltn2 q C) (apply_cltn2 r C) (apply_cltn2 s C)
[PROOF STEP]
from \<open>p \<noteq> q\<close> and \<open>r \<noteq> p\<close> and \<open>s \<noteq> p\<close> and \<open>r \<noteq> q\<close> and apply_cltn2_injective
[PROOF STATE]
proof (chain)
picking this:
p \<noteq> q
r \<noteq> p
s \<noteq> p
r \<noteq> q
apply_cltn2 ?p ?C = apply_cltn2 ?q ?C \<Longrightarrow> ?p = ?q
[PROOF STEP]
have "?pC \<noteq> ?qC" and "?rC \<noteq> ?pC" and "?sC \<noteq> ?pC" and "?rC \<noteq> ?qC"
[PROOF STATE]
proof (prove)
using this:
p \<noteq> q
r \<noteq> p
s \<noteq> p
r \<noteq> q
apply_cltn2 ?p ?C = apply_cltn2 ?q ?C \<Longrightarrow> ?p = ?q

goal (1 subgoal):
 1. (apply_cltn2 p C \<noteq> apply_cltn2 q C &&& apply_cltn2 r C \<noteq> apply_cltn2 p C) &&& apply_cltn2 s C \<noteq> apply_cltn2 p C &&& apply_cltn2 r C \<noteq> apply_cltn2 q C
[PROOF STEP]
by fast+
[PROOF STATE]
proof (state)
this:
apply_cltn2 p C \<noteq> apply_cltn2 q C
apply_cltn2 r C \<noteq> apply_cltn2 p C
apply_cltn2 s C \<noteq> apply_cltn2 p C
apply_cltn2 r C \<noteq> apply_cltn2 q C

goal (1 subgoal):
 1. cross_ratio_correct (apply_cltn2 p C) (apply_cltn2 q C) (apply_cltn2 r C) (apply_cltn2 s C)
[PROOF STEP]
with \<open>proj2_set_Col {?pC,?qC,?rC,?sC}\<close>
[PROOF STATE]
proof (chain)
picking this:
proj2_set_Col {apply_cltn2 p C, apply_cltn2 q C, apply_cltn2 r C, apply_cltn2 s C}
apply_cltn2 p C \<noteq> apply_cltn2 q C
apply_cltn2 r C \<noteq> apply_cltn2 p C
apply_cltn2 s C \<noteq> apply_cltn2 p C
apply_cltn2 r C \<noteq> apply_cltn2 q C
[PROOF STEP]
show "cross_ratio_correct ?pC ?qC ?rC ?sC"
[PROOF STATE]
proof (prove)
using this:
proj2_set_Col {apply_cltn2 p C, apply_cltn2 q C, apply_cltn2 r C, apply_cltn2 s C}
apply_cltn2 p C \<noteq> apply_cltn2 q C
apply_cltn2 r C \<noteq> apply_cltn2 p C
apply_cltn2 s C \<noteq> apply_cltn2 p C
apply_cltn2 r C \<noteq> apply_cltn2 q C

goal (1 subgoal):
 1. cross_ratio_correct (apply_cltn2 p C) (apply_cltn2 q C) (apply_cltn2 r C) (apply_cltn2 s C)
[PROOF STEP]
by (unfold cross_ratio_correct_def) simp
[PROOF STATE]
proof (state)
this:
cross_ratio_correct (apply_cltn2 p C) (apply_cltn2 q C) (apply_cltn2 r C) (apply_cltn2 s C)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cross_ratio_cltn2:
  assumes "proj2_set_Col {p,q,r,s}" and "p \<noteq> q" and "r \<noteq> p" and "s \<noteq> p"
  shows "cross_ratio (apply_cltn2 p C) (apply_cltn2 q C)
  (apply_cltn2 r C) (apply_cltn2 s C)
  = cross_ratio p q r s"
  (is "cross_ratio ?pC ?qC ?rC ?sC = _")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cross_ratio (apply_cltn2 p C) (apply_cltn2 q C) (apply_cltn2 r C) (apply_cltn2 s C) = cross_ratio p q r s
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cross_ratio (apply_cltn2 p C) (apply_cltn2 q C) (apply_cltn2 r C) (apply_cltn2 s C) = cross_ratio p q r s
[PROOF STEP]
let ?u = "proj2_rep p"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cross_ratio (apply_cltn2 p C) (apply_cltn2 q C) (apply_cltn2 r C) (apply_cltn2 s C) = cross_ratio p q r s
[PROOF STEP]
let ?v = "proj2_rep q"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cross_ratio (apply_cltn2 p C) (apply_cltn2 q C) (apply_cltn2 r C) (apply_cltn2 s C) = cross_ratio p q r s
[PROOF STEP]
let ?i = "proj2_Col_coeff p q r"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cross_ratio (apply_cltn2 p C) (apply_cltn2 q C) (apply_cltn2 r C) (apply_cltn2 s C) = cross_ratio p q r s
[PROOF STEP]
let ?j = "proj2_Col_coeff p q s"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cross_ratio (apply_cltn2 p C) (apply_cltn2 q C) (apply_cltn2 r C) (apply_cltn2 s C) = cross_ratio p q r s
[PROOF STEP]
from \<open>proj2_set_Col {p,q,r,s}\<close> and \<open>p \<noteq> q\<close> and \<open>r \<noteq> p\<close> and \<open>s \<noteq> p\<close>
    and proj2_set_Col_coeff
[PROOF STATE]
proof (chain)
picking this:
proj2_set_Col {p, q, r, s}
p \<noteq> q
r \<noteq> p
s \<noteq> p
\<lbrakk>proj2_set_Col ?S; {?p, ?q, ?r} \<subseteq> ?S; ?p \<noteq> ?q; ?r \<noteq> ?p\<rbrakk> \<Longrightarrow> ?r = proj2_abs (proj2_Col_coeff ?p ?q ?r *\<^sub>R proj2_rep ?p + proj2_rep ?q)
[PROOF STEP]
have "r = proj2_abs (?i *\<^sub>R ?u + ?v)" and "s = proj2_abs (?j *\<^sub>R ?u + ?v)"
[PROOF STATE]
proof (prove)
using this:
proj2_set_Col {p, q, r, s}
p \<noteq> q
r \<noteq> p
s \<noteq> p
\<lbrakk>proj2_set_Col ?S; {?p, ?q, ?r} \<subseteq> ?S; ?p \<noteq> ?q; ?r \<noteq> ?p\<rbrakk> \<Longrightarrow> ?r = proj2_abs (proj2_Col_coeff ?p ?q ?r *\<^sub>R proj2_rep ?p + proj2_rep ?q)

goal (1 subgoal):
 1. r = proj2_abs (proj2_Col_coeff p q r *\<^sub>R proj2_rep p + proj2_rep q) &&& s = proj2_abs (proj2_Col_coeff p q s *\<^sub>R proj2_rep p + proj2_rep q)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
r = proj2_abs (proj2_Col_coeff p q r *\<^sub>R proj2_rep p + proj2_rep q)
s = proj2_abs (proj2_Col_coeff p q s *\<^sub>R proj2_rep p + proj2_rep q)

goal (1 subgoal):
 1. cross_ratio (apply_cltn2 p C) (apply_cltn2 q C) (apply_cltn2 r C) (apply_cltn2 s C) = cross_ratio p q r s
[PROOF STEP]
let ?uC = "?u v* cltn2_rep C"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cross_ratio (apply_cltn2 p C) (apply_cltn2 q C) (apply_cltn2 r C) (apply_cltn2 s C) = cross_ratio p q r s
[PROOF STEP]
let ?vC = "?v v* cltn2_rep C"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cross_ratio (apply_cltn2 p C) (apply_cltn2 q C) (apply_cltn2 r C) (apply_cltn2 s C) = cross_ratio p q r s
[PROOF STEP]
have "?uC \<noteq> 0" and "?vC \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_rep p v* cltn2_rep C \<noteq> 0 &&& proj2_rep q v* cltn2_rep C \<noteq> 0
[PROOF STEP]
by (rule rep_mult_rep_non_zero)+
[PROOF STATE]
proof (state)
this:
proj2_rep p v* cltn2_rep C \<noteq> 0
proj2_rep q v* cltn2_rep C \<noteq> 0

goal (1 subgoal):
 1. cross_ratio (apply_cltn2 p C) (apply_cltn2 q C) (apply_cltn2 r C) (apply_cltn2 s C) = cross_ratio p q r s
[PROOF STEP]
have "proj2_abs ?uC = ?pC" and "proj2_abs ?vC = ?qC"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_abs (proj2_rep p v* cltn2_rep C) = apply_cltn2 p C &&& proj2_abs (proj2_rep q v* cltn2_rep C) = apply_cltn2 q C
[PROOF STEP]
by (unfold apply_cltn2_def) simp_all
[PROOF STATE]
proof (state)
this:
proj2_abs (proj2_rep p v* cltn2_rep C) = apply_cltn2 p C
proj2_abs (proj2_rep q v* cltn2_rep C) = apply_cltn2 q C

goal (1 subgoal):
 1. cross_ratio (apply_cltn2 p C) (apply_cltn2 q C) (apply_cltn2 r C) (apply_cltn2 s C) = cross_ratio p q r s
[PROOF STEP]
from \<open>p \<noteq> q\<close> and apply_cltn2_injective
[PROOF STATE]
proof (chain)
picking this:
p \<noteq> q
apply_cltn2 ?p ?C = apply_cltn2 ?q ?C \<Longrightarrow> ?p = ?q
[PROOF STEP]
have "?pC \<noteq> ?qC"
[PROOF STATE]
proof (prove)
using this:
p \<noteq> q
apply_cltn2 ?p ?C = apply_cltn2 ?q ?C \<Longrightarrow> ?p = ?q

goal (1 subgoal):
 1. apply_cltn2 p C \<noteq> apply_cltn2 q C
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
apply_cltn2 p C \<noteq> apply_cltn2 q C

goal (1 subgoal):
 1. cross_ratio (apply_cltn2 p C) (apply_cltn2 q C) (apply_cltn2 r C) (apply_cltn2 s C) = cross_ratio p q r s
[PROOF STEP]
from \<open>p \<noteq> q\<close> and proj2_rep_dependent [of _ p 1 q]
[PROOF STATE]
proof (chain)
picking this:
p \<noteq> q
\<lbrakk>?i *\<^sub>R proj2_rep p + 1 *\<^sub>R proj2_rep q = 0; ?i \<noteq> 0 \<or> 1 \<noteq> 0\<rbrakk> \<Longrightarrow> p = q
[PROOF STEP]
have "?i *\<^sub>R ?u + ?v \<noteq> 0" and "?j *\<^sub>R ?u + ?v \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
p \<noteq> q
\<lbrakk>?i *\<^sub>R proj2_rep p + 1 *\<^sub>R proj2_rep q = 0; ?i \<noteq> 0 \<or> 1 \<noteq> 0\<rbrakk> \<Longrightarrow> p = q

goal (1 subgoal):
 1. proj2_Col_coeff p q r *\<^sub>R proj2_rep p + proj2_rep q \<noteq> 0 &&& proj2_Col_coeff p q s *\<^sub>R proj2_rep p + proj2_rep q \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
proj2_Col_coeff p q r *\<^sub>R proj2_rep p + proj2_rep q \<noteq> 0
proj2_Col_coeff p q s *\<^sub>R proj2_rep p + proj2_rep q \<noteq> 0

goal (1 subgoal):
 1. cross_ratio (apply_cltn2 p C) (apply_cltn2 q C) (apply_cltn2 r C) (apply_cltn2 s C) = cross_ratio p q r s
[PROOF STEP]
with \<open>r = proj2_abs (?i *\<^sub>R ?u + ?v)\<close> and \<open>s = proj2_abs (?j *\<^sub>R ?u + ?v)\<close>
    and apply_cltn2_linear [of ?i ?u 1 ?v]
    and apply_cltn2_linear [of ?j ?u 1 ?v]
[PROOF STATE]
proof (chain)
picking this:
r = proj2_abs (proj2_Col_coeff p q r *\<^sub>R proj2_rep p + proj2_rep q)
s = proj2_abs (proj2_Col_coeff p q s *\<^sub>R proj2_rep p + proj2_rep q)
proj2_Col_coeff p q r *\<^sub>R proj2_rep p + 1 *\<^sub>R proj2_rep q \<noteq> 0 \<Longrightarrow> proj2_Col_coeff p q r *\<^sub>R (proj2_rep p v* cltn2_rep ?C) + 1 *\<^sub>R (proj2_rep q v* cltn2_rep ?C) \<noteq> 0
proj2_Col_coeff p q r *\<^sub>R proj2_rep p + 1 *\<^sub>R proj2_rep q \<noteq> 0 \<Longrightarrow> apply_cltn2 (proj2_abs (proj2_Col_coeff p q r *\<^sub>R proj2_rep p + 1 *\<^sub>R proj2_rep q)) ?C = proj2_abs (proj2_Col_coeff p q r *\<^sub>R (proj2_rep p v* cltn2_rep ?C) + 1 *\<^sub>R (proj2_rep q v* cltn2_rep ?C))
proj2_Col_coeff p q s *\<^sub>R proj2_rep p + 1 *\<^sub>R proj2_rep q \<noteq> 0 \<Longrightarrow> proj2_Col_coeff p q s *\<^sub>R (proj2_rep p v* cltn2_rep ?C) + 1 *\<^sub>R (proj2_rep q v* cltn2_rep ?C) \<noteq> 0
proj2_Col_coeff p q s *\<^sub>R proj2_rep p + 1 *\<^sub>R proj2_rep q \<noteq> 0 \<Longrightarrow> apply_cltn2 (proj2_abs (proj2_Col_coeff p q s *\<^sub>R proj2_rep p + 1 *\<^sub>R proj2_rep q)) ?C = proj2_abs (proj2_Col_coeff p q s *\<^sub>R (proj2_rep p v* cltn2_rep ?C) + 1 *\<^sub>R (proj2_rep q v* cltn2_rep ?C))
proj2_Col_coeff p q r *\<^sub>R proj2_rep p + proj2_rep q \<noteq> 0
proj2_Col_coeff p q s *\<^sub>R proj2_rep p + proj2_rep q \<noteq> 0
[PROOF STEP]
have "?rC = proj2_abs (?i *\<^sub>R ?uC + ?vC)"
    and "?sC = proj2_abs (?j *\<^sub>R ?uC + ?vC)"
[PROOF STATE]
proof (prove)
using this:
r = proj2_abs (proj2_Col_coeff p q r *\<^sub>R proj2_rep p + proj2_rep q)
s = proj2_abs (proj2_Col_coeff p q s *\<^sub>R proj2_rep p + proj2_rep q)
proj2_Col_coeff p q r *\<^sub>R proj2_rep p + 1 *\<^sub>R proj2_rep q \<noteq> 0 \<Longrightarrow> proj2_Col_coeff p q r *\<^sub>R (proj2_rep p v* cltn2_rep ?C) + 1 *\<^sub>R (proj2_rep q v* cltn2_rep ?C) \<noteq> 0
proj2_Col_coeff p q r *\<^sub>R proj2_rep p + 1 *\<^sub>R proj2_rep q \<noteq> 0 \<Longrightarrow> apply_cltn2 (proj2_abs (proj2_Col_coeff p q r *\<^sub>R proj2_rep p + 1 *\<^sub>R proj2_rep q)) ?C = proj2_abs (proj2_Col_coeff p q r *\<^sub>R (proj2_rep p v* cltn2_rep ?C) + 1 *\<^sub>R (proj2_rep q v* cltn2_rep ?C))
proj2_Col_coeff p q s *\<^sub>R proj2_rep p + 1 *\<^sub>R proj2_rep q \<noteq> 0 \<Longrightarrow> proj2_Col_coeff p q s *\<^sub>R (proj2_rep p v* cltn2_rep ?C) + 1 *\<^sub>R (proj2_rep q v* cltn2_rep ?C) \<noteq> 0
proj2_Col_coeff p q s *\<^sub>R proj2_rep p + 1 *\<^sub>R proj2_rep q \<noteq> 0 \<Longrightarrow> apply_cltn2 (proj2_abs (proj2_Col_coeff p q s *\<^sub>R proj2_rep p + 1 *\<^sub>R proj2_rep q)) ?C = proj2_abs (proj2_Col_coeff p q s *\<^sub>R (proj2_rep p v* cltn2_rep ?C) + 1 *\<^sub>R (proj2_rep q v* cltn2_rep ?C))
proj2_Col_coeff p q r *\<^sub>R proj2_rep p + proj2_rep q \<noteq> 0
proj2_Col_coeff p q s *\<^sub>R proj2_rep p + proj2_rep q \<noteq> 0

goal (1 subgoal):
 1. apply_cltn2 r C = proj2_abs (proj2_Col_coeff p q r *\<^sub>R (proj2_rep p v* cltn2_rep C) + proj2_rep q v* cltn2_rep C) &&& apply_cltn2 s C = proj2_abs (proj2_Col_coeff p q s *\<^sub>R (proj2_rep p v* cltn2_rep C) + proj2_rep q v* cltn2_rep C)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
apply_cltn2 r C = proj2_abs (proj2_Col_coeff p q r *\<^sub>R (proj2_rep p v* cltn2_rep C) + proj2_rep q v* cltn2_rep C)
apply_cltn2 s C = proj2_abs (proj2_Col_coeff p q s *\<^sub>R (proj2_rep p v* cltn2_rep C) + proj2_rep q v* cltn2_rep C)

goal (1 subgoal):
 1. cross_ratio (apply_cltn2 p C) (apply_cltn2 q C) (apply_cltn2 r C) (apply_cltn2 s C) = cross_ratio p q r s
[PROOF STEP]
with \<open>?uC \<noteq> 0\<close> and \<open>?vC \<noteq> 0\<close> and \<open>proj2_abs ?uC = ?pC\<close>
    and \<open>proj2_abs ?vC = ?qC\<close> and \<open>?pC \<noteq> ?qC\<close>
    and cross_ratio_abs [of ?uC ?vC 1 1 ?i ?j]
[PROOF STATE]
proof (chain)
picking this:
proj2_rep p v* cltn2_rep C \<noteq> 0
proj2_rep q v* cltn2_rep C \<noteq> 0
proj2_abs (proj2_rep p v* cltn2_rep C) = apply_cltn2 p C
proj2_abs (proj2_rep q v* cltn2_rep C) = apply_cltn2 q C
apply_cltn2 p C \<noteq> apply_cltn2 q C
\<lbrakk>proj2_rep p v* cltn2_rep C \<noteq> 0; proj2_rep q v* cltn2_rep C \<noteq> 0; proj2_abs (proj2_rep p v* cltn2_rep C) \<noteq> proj2_abs (proj2_rep q v* cltn2_rep C); 1 \<noteq> 0; 1 \<noteq> 0\<rbrakk> \<Longrightarrow> cross_ratio (proj2_abs (proj2_rep p v* cltn2_rep C)) (proj2_abs (proj2_rep q v* cltn2_rep C)) (proj2_abs (proj2_Col_coeff p q r *\<^sub>R (proj2_rep p v* cltn2_rep C) + 1 *\<^sub>R (proj2_rep q v* cltn2_rep C))) (proj2_abs (proj2_Col_coeff p q s *\<^sub>R (proj2_rep p v* cltn2_rep C) + 1 *\<^sub>R (proj2_rep q v* cltn2_rep C))) = 1 * proj2_Col_coeff p q s / (proj2_Col_coeff p q r * 1)
apply_cltn2 r C = proj2_abs (proj2_Col_coeff p q r *\<^sub>R (proj2_rep p v* cltn2_rep C) + proj2_rep q v* cltn2_rep C)
apply_cltn2 s C = proj2_abs (proj2_Col_coeff p q s *\<^sub>R (proj2_rep p v* cltn2_rep C) + proj2_rep q v* cltn2_rep C)
[PROOF STEP]
have "cross_ratio ?pC ?qC ?rC ?sC = ?j/?i"
[PROOF STATE]
proof (prove)
using this:
proj2_rep p v* cltn2_rep C \<noteq> 0
proj2_rep q v* cltn2_rep C \<noteq> 0
proj2_abs (proj2_rep p v* cltn2_rep C) = apply_cltn2 p C
proj2_abs (proj2_rep q v* cltn2_rep C) = apply_cltn2 q C
apply_cltn2 p C \<noteq> apply_cltn2 q C
\<lbrakk>proj2_rep p v* cltn2_rep C \<noteq> 0; proj2_rep q v* cltn2_rep C \<noteq> 0; proj2_abs (proj2_rep p v* cltn2_rep C) \<noteq> proj2_abs (proj2_rep q v* cltn2_rep C); 1 \<noteq> 0; 1 \<noteq> 0\<rbrakk> \<Longrightarrow> cross_ratio (proj2_abs (proj2_rep p v* cltn2_rep C)) (proj2_abs (proj2_rep q v* cltn2_rep C)) (proj2_abs (proj2_Col_coeff p q r *\<^sub>R (proj2_rep p v* cltn2_rep C) + 1 *\<^sub>R (proj2_rep q v* cltn2_rep C))) (proj2_abs (proj2_Col_coeff p q s *\<^sub>R (proj2_rep p v* cltn2_rep C) + 1 *\<^sub>R (proj2_rep q v* cltn2_rep C))) = 1 * proj2_Col_coeff p q s / (proj2_Col_coeff p q r * 1)
apply_cltn2 r C = proj2_abs (proj2_Col_coeff p q r *\<^sub>R (proj2_rep p v* cltn2_rep C) + proj2_rep q v* cltn2_rep C)
apply_cltn2 s C = proj2_abs (proj2_Col_coeff p q s *\<^sub>R (proj2_rep p v* cltn2_rep C) + proj2_rep q v* cltn2_rep C)

goal (1 subgoal):
 1. cross_ratio (apply_cltn2 p C) (apply_cltn2 q C) (apply_cltn2 r C) (apply_cltn2 s C) = proj2_Col_coeff p q s / proj2_Col_coeff p q r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cross_ratio (apply_cltn2 p C) (apply_cltn2 q C) (apply_cltn2 r C) (apply_cltn2 s C) = proj2_Col_coeff p q s / proj2_Col_coeff p q r

goal (1 subgoal):
 1. cross_ratio (apply_cltn2 p C) (apply_cltn2 q C) (apply_cltn2 r C) (apply_cltn2 s C) = cross_ratio p q r s
[PROOF STEP]
thus "cross_ratio ?pC ?qC ?rC ?sC = cross_ratio p q r s"
[PROOF STATE]
proof (prove)
using this:
cross_ratio (apply_cltn2 p C) (apply_cltn2 q C) (apply_cltn2 r C) (apply_cltn2 s C) = proj2_Col_coeff p q s / proj2_Col_coeff p q r

goal (1 subgoal):
 1. cross_ratio (apply_cltn2 p C) (apply_cltn2 q C) (apply_cltn2 r C) (apply_cltn2 s C) = cross_ratio p q r s
[PROOF STEP]
unfolding cross_ratio_def [of p q r s]
[PROOF STATE]
proof (prove)
using this:
cross_ratio (apply_cltn2 p C) (apply_cltn2 q C) (apply_cltn2 r C) (apply_cltn2 s C) = proj2_Col_coeff p q s / proj2_Col_coeff p q r

goal (1 subgoal):
 1. cross_ratio (apply_cltn2 p C) (apply_cltn2 q C) (apply_cltn2 r C) (apply_cltn2 s C) = proj2_Col_coeff p q s / proj2_Col_coeff p q r
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
cross_ratio (apply_cltn2 p C) (apply_cltn2 q C) (apply_cltn2 r C) (apply_cltn2 s C) = cross_ratio p q r s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cross_ratio_unique:
  assumes "cross_ratio_correct p q r s" and "cross_ratio_correct p q r t"
  and "cross_ratio p q r s = cross_ratio p q r t"
  shows "s = t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s = t
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s = t
[PROOF STEP]
from \<open>cross_ratio_correct p q r s\<close> and \<open>cross_ratio_correct p q r t\<close>
[PROOF STATE]
proof (chain)
picking this:
cross_ratio_correct p q r s
cross_ratio_correct p q r t
[PROOF STEP]
have "proj2_set_Col {p,q,r,s}" and "proj2_set_Col {p,q,r,t}"
    and "p \<noteq> q" and "r \<noteq> p" and "r \<noteq> q" and "s \<noteq> p" and "t \<noteq> p"
[PROOF STATE]
proof (prove)
using this:
cross_ratio_correct p q r s
cross_ratio_correct p q r t

goal (1 subgoal):
 1. (proj2_set_Col {p, q, r, s} &&& proj2_set_Col {p, q, r, t} &&& p \<noteq> q) &&& (r \<noteq> p &&& r \<noteq> q) &&& s \<noteq> p &&& t \<noteq> p
[PROOF STEP]
by (unfold cross_ratio_correct_def) simp_all
[PROOF STATE]
proof (state)
this:
proj2_set_Col {p, q, r, s}
proj2_set_Col {p, q, r, t}
p \<noteq> q
r \<noteq> p
r \<noteq> q
s \<noteq> p
t \<noteq> p

goal (1 subgoal):
 1. s = t
[PROOF STEP]
let ?u = "proj2_rep p"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s = t
[PROOF STEP]
let ?v = "proj2_rep q"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s = t
[PROOF STEP]
let ?i = "proj2_Col_coeff p q r"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s = t
[PROOF STEP]
let ?j = "proj2_Col_coeff p q s"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s = t
[PROOF STEP]
let ?k = "proj2_Col_coeff p q t"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s = t
[PROOF STEP]
from \<open>proj2_set_Col {p,q,r,s}\<close> and \<open>proj2_set_Col {p,q,r,t}\<close>
    and \<open>p \<noteq> q\<close> and \<open>r \<noteq> p\<close> and \<open>s \<noteq> p\<close> and \<open>t \<noteq> p\<close> and proj2_set_Col_coeff
[PROOF STATE]
proof (chain)
picking this:
proj2_set_Col {p, q, r, s}
proj2_set_Col {p, q, r, t}
p \<noteq> q
r \<noteq> p
s \<noteq> p
t \<noteq> p
\<lbrakk>proj2_set_Col ?S; {?p, ?q, ?r} \<subseteq> ?S; ?p \<noteq> ?q; ?r \<noteq> ?p\<rbrakk> \<Longrightarrow> ?r = proj2_abs (proj2_Col_coeff ?p ?q ?r *\<^sub>R proj2_rep ?p + proj2_rep ?q)
[PROOF STEP]
have "r = proj2_abs (?i *\<^sub>R ?u + ?v)"
    and "s = proj2_abs (?j *\<^sub>R ?u + ?v)"
    and "t = proj2_abs (?k *\<^sub>R ?u + ?v)"
[PROOF STATE]
proof (prove)
using this:
proj2_set_Col {p, q, r, s}
proj2_set_Col {p, q, r, t}
p \<noteq> q
r \<noteq> p
s \<noteq> p
t \<noteq> p
\<lbrakk>proj2_set_Col ?S; {?p, ?q, ?r} \<subseteq> ?S; ?p \<noteq> ?q; ?r \<noteq> ?p\<rbrakk> \<Longrightarrow> ?r = proj2_abs (proj2_Col_coeff ?p ?q ?r *\<^sub>R proj2_rep ?p + proj2_rep ?q)

goal (1 subgoal):
 1. r = proj2_abs (proj2_Col_coeff p q r *\<^sub>R proj2_rep p + proj2_rep q) &&& s = proj2_abs (proj2_Col_coeff p q s *\<^sub>R proj2_rep p + proj2_rep q) &&& t = proj2_abs (proj2_Col_coeff p q t *\<^sub>R proj2_rep p + proj2_rep q)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
r = proj2_abs (proj2_Col_coeff p q r *\<^sub>R proj2_rep p + proj2_rep q)
s = proj2_abs (proj2_Col_coeff p q s *\<^sub>R proj2_rep p + proj2_rep q)
t = proj2_abs (proj2_Col_coeff p q t *\<^sub>R proj2_rep p + proj2_rep q)

goal (1 subgoal):
 1. s = t
[PROOF STEP]
from \<open>r \<noteq> q\<close> and \<open>r = proj2_abs (?i *\<^sub>R ?u + ?v)\<close>
[PROOF STATE]
proof (chain)
picking this:
r \<noteq> q
r = proj2_abs (proj2_Col_coeff p q r *\<^sub>R proj2_rep p + proj2_rep q)
[PROOF STEP]
have "?i \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
r \<noteq> q
r = proj2_abs (proj2_Col_coeff p q r *\<^sub>R proj2_rep p + proj2_rep q)

goal (1 subgoal):
 1. proj2_Col_coeff p q r \<noteq> 0
[PROOF STEP]
by (auto simp add: proj2_abs_rep)
[PROOF STATE]
proof (state)
this:
proj2_Col_coeff p q r \<noteq> 0

goal (1 subgoal):
 1. s = t
[PROOF STEP]
with \<open>cross_ratio p q r s = cross_ratio p q r t\<close>
[PROOF STATE]
proof (chain)
picking this:
cross_ratio p q r s = cross_ratio p q r t
proj2_Col_coeff p q r \<noteq> 0
[PROOF STEP]
have "?j = ?k"
[PROOF STATE]
proof (prove)
using this:
cross_ratio p q r s = cross_ratio p q r t
proj2_Col_coeff p q r \<noteq> 0

goal (1 subgoal):
 1. proj2_Col_coeff p q s = proj2_Col_coeff p q t
[PROOF STEP]
by (unfold cross_ratio_def) simp
[PROOF STATE]
proof (state)
this:
proj2_Col_coeff p q s = proj2_Col_coeff p q t

goal (1 subgoal):
 1. s = t
[PROOF STEP]
with \<open>s = proj2_abs (?j *\<^sub>R ?u + ?v)\<close> and \<open>t = proj2_abs (?k *\<^sub>R ?u + ?v)\<close>
[PROOF STATE]
proof (chain)
picking this:
s = proj2_abs (proj2_Col_coeff p q s *\<^sub>R proj2_rep p + proj2_rep q)
t = proj2_abs (proj2_Col_coeff p q t *\<^sub>R proj2_rep p + proj2_rep q)
proj2_Col_coeff p q s = proj2_Col_coeff p q t
[PROOF STEP]
show "s = t"
[PROOF STATE]
proof (prove)
using this:
s = proj2_abs (proj2_Col_coeff p q s *\<^sub>R proj2_rep p + proj2_rep q)
t = proj2_abs (proj2_Col_coeff p q t *\<^sub>R proj2_rep p + proj2_rep q)
proj2_Col_coeff p q s = proj2_Col_coeff p q t

goal (1 subgoal):
 1. s = t
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
s = t

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cltn2_three_point_line:
  assumes "p \<noteq> q" and "r \<noteq> p" and "r \<noteq> q"
  and "proj2_incident p l" and "proj2_incident q l" and "proj2_incident r l"
  and "apply_cltn2 p C = p" and "apply_cltn2 q C = q" and "apply_cltn2 r C = r"
  and "proj2_incident s l"
  shows "apply_cltn2 s C = s" (is "?sC = s")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. apply_cltn2 s C = s
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> apply_cltn2 s C = s
 2. \<not> ?P \<Longrightarrow> apply_cltn2 s C = s
[PROOF STEP]
assume "s = p"
[PROOF STATE]
proof (state)
this:
s = p

goal (2 subgoals):
 1. ?P \<Longrightarrow> apply_cltn2 s C = s
 2. \<not> ?P \<Longrightarrow> apply_cltn2 s C = s
[PROOF STEP]
with \<open>apply_cltn2 p C = p\<close>
[PROOF STATE]
proof (chain)
picking this:
apply_cltn2 p C = p
s = p
[PROOF STEP]
show "?sC = s"
[PROOF STATE]
proof (prove)
using this:
apply_cltn2 p C = p
s = p

goal (1 subgoal):
 1. apply_cltn2 s C = s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
apply_cltn2 s C = s

goal (1 subgoal):
 1. s \<noteq> p \<Longrightarrow> apply_cltn2 s C = s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s \<noteq> p \<Longrightarrow> apply_cltn2 s C = s
[PROOF STEP]
assume "s \<noteq> p"
[PROOF STATE]
proof (state)
this:
s \<noteq> p

goal (1 subgoal):
 1. s \<noteq> p \<Longrightarrow> apply_cltn2 s C = s
[PROOF STEP]
let ?pC = "apply_cltn2 p C"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s \<noteq> p \<Longrightarrow> apply_cltn2 s C = s
[PROOF STEP]
let ?qC = "apply_cltn2 q C"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s \<noteq> p \<Longrightarrow> apply_cltn2 s C = s
[PROOF STEP]
let ?rC = "apply_cltn2 r C"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s \<noteq> p \<Longrightarrow> apply_cltn2 s C = s
[PROOF STEP]
from \<open>proj2_incident p l\<close> and \<open>proj2_incident q l\<close> and \<open>proj2_incident r l\<close>
    and \<open>proj2_incident s l\<close>
[PROOF STATE]
proof (chain)
picking this:
proj2_incident p l
proj2_incident q l
proj2_incident r l
proj2_incident s l
[PROOF STEP]
have "proj2_set_Col {p,q,r,s}"
[PROOF STATE]
proof (prove)
using this:
proj2_incident p l
proj2_incident q l
proj2_incident r l
proj2_incident s l

goal (1 subgoal):
 1. proj2_set_Col {p, q, r, s}
[PROOF STEP]
by (unfold proj2_set_Col_def) auto
[PROOF STATE]
proof (state)
this:
proj2_set_Col {p, q, r, s}

goal (1 subgoal):
 1. s \<noteq> p \<Longrightarrow> apply_cltn2 s C = s
[PROOF STEP]
with \<open>p \<noteq> q\<close> and \<open>r \<noteq> p\<close> and \<open>s \<noteq> p\<close> and \<open>r \<noteq> q\<close>
[PROOF STATE]
proof (chain)
picking this:
p \<noteq> q
r \<noteq> p
s \<noteq> p
r \<noteq> q
proj2_set_Col {p, q, r, s}
[PROOF STEP]
have "cross_ratio_correct p q r s"
[PROOF STATE]
proof (prove)
using this:
p \<noteq> q
r \<noteq> p
s \<noteq> p
r \<noteq> q
proj2_set_Col {p, q, r, s}

goal (1 subgoal):
 1. cross_ratio_correct p q r s
[PROOF STEP]
by (unfold cross_ratio_correct_def) simp
[PROOF STATE]
proof (state)
this:
cross_ratio_correct p q r s

goal (1 subgoal):
 1. s \<noteq> p \<Longrightarrow> apply_cltn2 s C = s
[PROOF STEP]
hence "cross_ratio_correct ?pC ?qC ?rC ?sC"
[PROOF STATE]
proof (prove)
using this:
cross_ratio_correct p q r s

goal (1 subgoal):
 1. cross_ratio_correct (apply_cltn2 p C) (apply_cltn2 q C) (apply_cltn2 r C) (apply_cltn2 s C)
[PROOF STEP]
by (rule cross_ratio_correct_cltn2)
[PROOF STATE]
proof (state)
this:
cross_ratio_correct (apply_cltn2 p C) (apply_cltn2 q C) (apply_cltn2 r C) (apply_cltn2 s C)

goal (1 subgoal):
 1. s \<noteq> p \<Longrightarrow> apply_cltn2 s C = s
[PROOF STEP]
with \<open>?pC = p\<close> and \<open>?qC = q\<close> and \<open>?rC = r\<close>
[PROOF STATE]
proof (chain)
picking this:
apply_cltn2 p C = p
apply_cltn2 q C = q
apply_cltn2 r C = r
cross_ratio_correct (apply_cltn2 p C) (apply_cltn2 q C) (apply_cltn2 r C) (apply_cltn2 s C)
[PROOF STEP]
have "cross_ratio_correct p q r ?sC"
[PROOF STATE]
proof (prove)
using this:
apply_cltn2 p C = p
apply_cltn2 q C = q
apply_cltn2 r C = r
cross_ratio_correct (apply_cltn2 p C) (apply_cltn2 q C) (apply_cltn2 r C) (apply_cltn2 s C)

goal (1 subgoal):
 1. cross_ratio_correct p q r (apply_cltn2 s C)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cross_ratio_correct p q r (apply_cltn2 s C)

goal (1 subgoal):
 1. s \<noteq> p \<Longrightarrow> apply_cltn2 s C = s
[PROOF STEP]
from \<open>proj2_set_Col {p,q,r,s}\<close> and \<open>p \<noteq> q\<close> and \<open>r \<noteq> p\<close> and \<open>s \<noteq> p\<close>
[PROOF STATE]
proof (chain)
picking this:
proj2_set_Col {p, q, r, s}
p \<noteq> q
r \<noteq> p
s \<noteq> p
[PROOF STEP]
have "cross_ratio ?pC ?qC ?rC ?sC = cross_ratio p q r s"
[PROOF STATE]
proof (prove)
using this:
proj2_set_Col {p, q, r, s}
p \<noteq> q
r \<noteq> p
s \<noteq> p

goal (1 subgoal):
 1. cross_ratio (apply_cltn2 p C) (apply_cltn2 q C) (apply_cltn2 r C) (apply_cltn2 s C) = cross_ratio p q r s
[PROOF STEP]
by (rule cross_ratio_cltn2)
[PROOF STATE]
proof (state)
this:
cross_ratio (apply_cltn2 p C) (apply_cltn2 q C) (apply_cltn2 r C) (apply_cltn2 s C) = cross_ratio p q r s

goal (1 subgoal):
 1. s \<noteq> p \<Longrightarrow> apply_cltn2 s C = s
[PROOF STEP]
with \<open>?pC = p\<close> and \<open>?qC = q\<close> and \<open>?rC = r\<close>
[PROOF STATE]
proof (chain)
picking this:
apply_cltn2 p C = p
apply_cltn2 q C = q
apply_cltn2 r C = r
cross_ratio (apply_cltn2 p C) (apply_cltn2 q C) (apply_cltn2 r C) (apply_cltn2 s C) = cross_ratio p q r s
[PROOF STEP]
have "cross_ratio p q r ?sC = cross_ratio p q r s"
[PROOF STATE]
proof (prove)
using this:
apply_cltn2 p C = p
apply_cltn2 q C = q
apply_cltn2 r C = r
cross_ratio (apply_cltn2 p C) (apply_cltn2 q C) (apply_cltn2 r C) (apply_cltn2 s C) = cross_ratio p q r s

goal (1 subgoal):
 1. cross_ratio p q r (apply_cltn2 s C) = cross_ratio p q r s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cross_ratio p q r (apply_cltn2 s C) = cross_ratio p q r s

goal (1 subgoal):
 1. s \<noteq> p \<Longrightarrow> apply_cltn2 s C = s
[PROOF STEP]
with \<open>cross_ratio_correct p q r ?sC\<close> and \<open>cross_ratio_correct p q r s\<close>
[PROOF STATE]
proof (chain)
picking this:
cross_ratio_correct p q r (apply_cltn2 s C)
cross_ratio_correct p q r s
cross_ratio p q r (apply_cltn2 s C) = cross_ratio p q r s
[PROOF STEP]
show "?sC = s"
[PROOF STATE]
proof (prove)
using this:
cross_ratio_correct p q r (apply_cltn2 s C)
cross_ratio_correct p q r s
cross_ratio p q r (apply_cltn2 s C) = cross_ratio p q r s

goal (1 subgoal):
 1. apply_cltn2 s C = s
[PROOF STEP]
by (rule cross_ratio_unique)
[PROOF STATE]
proof (state)
this:
apply_cltn2 s C = s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cross_ratio_equal_cltn2:
  assumes "cross_ratio_correct p q r s"
  and "cross_ratio_correct (apply_cltn2 p C) (apply_cltn2 q C)
  (apply_cltn2 r C) t"
  (is "cross_ratio_correct ?pC ?qC ?rC t")
  and "cross_ratio (apply_cltn2 p C) (apply_cltn2 q C) (apply_cltn2 r C) t
    = cross_ratio p q r s"
  shows "t = apply_cltn2 s C" (is "t = ?sC")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t = apply_cltn2 s C
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. t = apply_cltn2 s C
[PROOF STEP]
from \<open>cross_ratio_correct p q r s\<close>
[PROOF STATE]
proof (chain)
picking this:
cross_ratio_correct p q r s
[PROOF STEP]
have "cross_ratio_correct ?pC ?qC ?rC ?sC"
[PROOF STATE]
proof (prove)
using this:
cross_ratio_correct p q r s

goal (1 subgoal):
 1. cross_ratio_correct (apply_cltn2 p C) (apply_cltn2 q C) (apply_cltn2 r C) (apply_cltn2 s C)
[PROOF STEP]
by (rule cross_ratio_correct_cltn2)
[PROOF STATE]
proof (state)
this:
cross_ratio_correct (apply_cltn2 p C) (apply_cltn2 q C) (apply_cltn2 r C) (apply_cltn2 s C)

goal (1 subgoal):
 1. t = apply_cltn2 s C
[PROOF STEP]
from \<open>cross_ratio_correct p q r s\<close>
[PROOF STATE]
proof (chain)
picking this:
cross_ratio_correct p q r s
[PROOF STEP]
have "proj2_set_Col {p,q,r,s}" and "p \<noteq> q" and "r \<noteq> p" and "s \<noteq> p"
[PROOF STATE]
proof (prove)
using this:
cross_ratio_correct p q r s

goal (1 subgoal):
 1. (proj2_set_Col {p, q, r, s} &&& p \<noteq> q) &&& r \<noteq> p &&& s \<noteq> p
[PROOF STEP]
by (unfold cross_ratio_correct_def) simp_all
[PROOF STATE]
proof (state)
this:
proj2_set_Col {p, q, r, s}
p \<noteq> q
r \<noteq> p
s \<noteq> p

goal (1 subgoal):
 1. t = apply_cltn2 s C
[PROOF STEP]
hence "cross_ratio ?pC ?qC ?rC ?sC = cross_ratio p q r s"
[PROOF STATE]
proof (prove)
using this:
proj2_set_Col {p, q, r, s}
p \<noteq> q
r \<noteq> p
s \<noteq> p

goal (1 subgoal):
 1. cross_ratio (apply_cltn2 p C) (apply_cltn2 q C) (apply_cltn2 r C) (apply_cltn2 s C) = cross_ratio p q r s
[PROOF STEP]
by (rule cross_ratio_cltn2)
[PROOF STATE]
proof (state)
this:
cross_ratio (apply_cltn2 p C) (apply_cltn2 q C) (apply_cltn2 r C) (apply_cltn2 s C) = cross_ratio p q r s

goal (1 subgoal):
 1. t = apply_cltn2 s C
[PROOF STEP]
with \<open>cross_ratio ?pC ?qC ?rC t = cross_ratio p q r s\<close>
[PROOF STATE]
proof (chain)
picking this:
cross_ratio (apply_cltn2 p C) (apply_cltn2 q C) (apply_cltn2 r C) t = cross_ratio p q r s
cross_ratio (apply_cltn2 p C) (apply_cltn2 q C) (apply_cltn2 r C) (apply_cltn2 s C) = cross_ratio p q r s
[PROOF STEP]
have "cross_ratio ?pC ?qC ?rC t = cross_ratio ?pC ?qC ?rC ?sC"
[PROOF STATE]
proof (prove)
using this:
cross_ratio (apply_cltn2 p C) (apply_cltn2 q C) (apply_cltn2 r C) t = cross_ratio p q r s
cross_ratio (apply_cltn2 p C) (apply_cltn2 q C) (apply_cltn2 r C) (apply_cltn2 s C) = cross_ratio p q r s

goal (1 subgoal):
 1. cross_ratio (apply_cltn2 p C) (apply_cltn2 q C) (apply_cltn2 r C) t = cross_ratio (apply_cltn2 p C) (apply_cltn2 q C) (apply_cltn2 r C) (apply_cltn2 s C)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cross_ratio (apply_cltn2 p C) (apply_cltn2 q C) (apply_cltn2 r C) t = cross_ratio (apply_cltn2 p C) (apply_cltn2 q C) (apply_cltn2 r C) (apply_cltn2 s C)

goal (1 subgoal):
 1. t = apply_cltn2 s C
[PROOF STEP]
with \<open>cross_ratio_correct ?pC ?qC ?rC t\<close>
    and \<open>cross_ratio_correct ?pC ?qC ?rC ?sC\<close>
[PROOF STATE]
proof (chain)
picking this:
cross_ratio_correct (apply_cltn2 p C) (apply_cltn2 q C) (apply_cltn2 r C) t
cross_ratio_correct (apply_cltn2 p C) (apply_cltn2 q C) (apply_cltn2 r C) (apply_cltn2 s C)
cross_ratio (apply_cltn2 p C) (apply_cltn2 q C) (apply_cltn2 r C) t = cross_ratio (apply_cltn2 p C) (apply_cltn2 q C) (apply_cltn2 r C) (apply_cltn2 s C)
[PROOF STEP]
show "t = ?sC"
[PROOF STATE]
proof (prove)
using this:
cross_ratio_correct (apply_cltn2 p C) (apply_cltn2 q C) (apply_cltn2 r C) t
cross_ratio_correct (apply_cltn2 p C) (apply_cltn2 q C) (apply_cltn2 r C) (apply_cltn2 s C)
cross_ratio (apply_cltn2 p C) (apply_cltn2 q C) (apply_cltn2 r C) t = cross_ratio (apply_cltn2 p C) (apply_cltn2 q C) (apply_cltn2 r C) (apply_cltn2 s C)

goal (1 subgoal):
 1. t = apply_cltn2 s C
[PROOF STEP]
by (rule cross_ratio_unique)
[PROOF STATE]
proof (state)
this:
t = apply_cltn2 s C

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proj2_Col_distinct_coeff_non_zero:
  assumes "proj2_Col p q r" and "p \<noteq> q" and "r \<noteq> p" and "r \<noteq> q"
  shows "proj2_Col_coeff p q r \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_Col_coeff p q r \<noteq> 0
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. proj2_Col_coeff p q r = 0 \<Longrightarrow> False
[PROOF STEP]
assume "proj2_Col_coeff p q r = 0"
[PROOF STATE]
proof (state)
this:
proj2_Col_coeff p q r = 0

goal (1 subgoal):
 1. proj2_Col_coeff p q r = 0 \<Longrightarrow> False
[PROOF STEP]
from \<open>proj2_Col p q r\<close> and \<open>p \<noteq> q\<close> and \<open>r \<noteq> p\<close>
[PROOF STATE]
proof (chain)
picking this:
proj2_Col p q r
p \<noteq> q
r \<noteq> p
[PROOF STEP]
have "r = proj2_abs ((proj2_Col_coeff p q r) *\<^sub>R proj2_rep p + proj2_rep q)"
[PROOF STATE]
proof (prove)
using this:
proj2_Col p q r
p \<noteq> q
r \<noteq> p

goal (1 subgoal):
 1. r = proj2_abs (proj2_Col_coeff p q r *\<^sub>R proj2_rep p + proj2_rep q)
[PROOF STEP]
by (rule proj2_Col_coeff)
[PROOF STATE]
proof (state)
this:
r = proj2_abs (proj2_Col_coeff p q r *\<^sub>R proj2_rep p + proj2_rep q)

goal (1 subgoal):
 1. proj2_Col_coeff p q r = 0 \<Longrightarrow> False
[PROOF STEP]
with \<open>proj2_Col_coeff p q r = 0\<close>
[PROOF STATE]
proof (chain)
picking this:
proj2_Col_coeff p q r = 0
r = proj2_abs (proj2_Col_coeff p q r *\<^sub>R proj2_rep p + proj2_rep q)
[PROOF STEP]
have "r = q"
[PROOF STATE]
proof (prove)
using this:
proj2_Col_coeff p q r = 0
r = proj2_abs (proj2_Col_coeff p q r *\<^sub>R proj2_rep p + proj2_rep q)

goal (1 subgoal):
 1. r = q
[PROOF STEP]
by (simp add: proj2_abs_rep)
[PROOF STATE]
proof (state)
this:
r = q

goal (1 subgoal):
 1. proj2_Col_coeff p q r = 0 \<Longrightarrow> False
[PROOF STEP]
with \<open>r \<noteq> q\<close>
[PROOF STATE]
proof (chain)
picking this:
r \<noteq> q
r = q
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
r \<noteq> q
r = q

goal (1 subgoal):
 1. False
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cross_ratio_product:
  assumes "proj2_Col p q s" and "p \<noteq> q" and "s \<noteq> p" and "s \<noteq> q"
  shows "cross_ratio p q r s * cross_ratio p q s t = cross_ratio p q r t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cross_ratio p q r s * cross_ratio p q s t = cross_ratio p q r t
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cross_ratio p q r s * cross_ratio p q s t = cross_ratio p q r t
[PROOF STEP]
from \<open>proj2_Col p q s\<close> and \<open>p \<noteq> q\<close> and \<open>s \<noteq> p\<close> and \<open>s \<noteq> q\<close>
[PROOF STATE]
proof (chain)
picking this:
proj2_Col p q s
p \<noteq> q
s \<noteq> p
s \<noteq> q
[PROOF STEP]
have "proj2_Col_coeff p q s \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
proj2_Col p q s
p \<noteq> q
s \<noteq> p
s \<noteq> q

goal (1 subgoal):
 1. proj2_Col_coeff p q s \<noteq> 0
[PROOF STEP]
by (rule proj2_Col_distinct_coeff_non_zero)
[PROOF STATE]
proof (state)
this:
proj2_Col_coeff p q s \<noteq> 0

goal (1 subgoal):
 1. cross_ratio p q r s * cross_ratio p q s t = cross_ratio p q r t
[PROOF STEP]
thus "cross_ratio p q r s * cross_ratio p q s t = cross_ratio p q r t"
[PROOF STATE]
proof (prove)
using this:
proj2_Col_coeff p q s \<noteq> 0

goal (1 subgoal):
 1. cross_ratio p q r s * cross_ratio p q s t = cross_ratio p q r t
[PROOF STEP]
by (unfold cross_ratio_def) simp
[PROOF STATE]
proof (state)
this:
cross_ratio p q r s * cross_ratio p q s t = cross_ratio p q r t

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cross_ratio_equal_1:
  assumes "proj2_Col p q r" and "p \<noteq> q" and "r \<noteq> p" and "r \<noteq> q"
  shows "cross_ratio p q r r = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cross_ratio p q r r = 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cross_ratio p q r r = 1
[PROOF STEP]
from \<open>proj2_Col p q r\<close> and \<open>p \<noteq> q\<close> and \<open>r \<noteq> p\<close> and \<open>r \<noteq> q\<close>
[PROOF STATE]
proof (chain)
picking this:
proj2_Col p q r
p \<noteq> q
r \<noteq> p
r \<noteq> q
[PROOF STEP]
have "proj2_Col_coeff p q r \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
proj2_Col p q r
p \<noteq> q
r \<noteq> p
r \<noteq> q

goal (1 subgoal):
 1. proj2_Col_coeff p q r \<noteq> 0
[PROOF STEP]
by (rule proj2_Col_distinct_coeff_non_zero)
[PROOF STATE]
proof (state)
this:
proj2_Col_coeff p q r \<noteq> 0

goal (1 subgoal):
 1. cross_ratio p q r r = 1
[PROOF STEP]
thus "cross_ratio p q r r = 1"
[PROOF STATE]
proof (prove)
using this:
proj2_Col_coeff p q r \<noteq> 0

goal (1 subgoal):
 1. cross_ratio p q r r = 1
[PROOF STEP]
by (unfold cross_ratio_def) simp
[PROOF STATE]
proof (state)
this:
cross_ratio p q r r = 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cross_ratio_1_equal:
  assumes "cross_ratio_correct p q r s" and "cross_ratio p q r s = 1"
  shows "r = s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r = s
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. r = s
[PROOF STEP]
from \<open>cross_ratio_correct p q r s\<close>
[PROOF STATE]
proof (chain)
picking this:
cross_ratio_correct p q r s
[PROOF STEP]
have "proj2_set_Col {p,q,r,s}" and "p \<noteq> q" and "r \<noteq> p" and "r \<noteq> q"
[PROOF STATE]
proof (prove)
using this:
cross_ratio_correct p q r s

goal (1 subgoal):
 1. (proj2_set_Col {p, q, r, s} &&& p \<noteq> q) &&& r \<noteq> p &&& r \<noteq> q
[PROOF STEP]
by (unfold cross_ratio_correct_def) simp_all
[PROOF STATE]
proof (state)
this:
proj2_set_Col {p, q, r, s}
p \<noteq> q
r \<noteq> p
r \<noteq> q

goal (1 subgoal):
 1. r = s
[PROOF STEP]
from \<open>proj2_set_Col {p,q,r,s}\<close>
[PROOF STATE]
proof (chain)
picking this:
proj2_set_Col {p, q, r, s}
[PROOF STEP]
have "proj2_set_Col {p,q,r}"
[PROOF STATE]
proof (prove)
using this:
proj2_set_Col {p, q, r, s}

goal (1 subgoal):
 1. proj2_set_Col {p, q, r}
[PROOF STEP]
by (simp add: proj2_subset_Col [of "{p,q,r}" "{p,q,r,s}"])
[PROOF STATE]
proof (state)
this:
proj2_set_Col {p, q, r}

goal (1 subgoal):
 1. r = s
[PROOF STEP]
with \<open>p \<noteq> q\<close> and \<open>r \<noteq> p\<close> and \<open>r \<noteq> q\<close>
[PROOF STATE]
proof (chain)
picking this:
p \<noteq> q
r \<noteq> p
r \<noteq> q
proj2_set_Col {p, q, r}
[PROOF STEP]
have "cross_ratio_correct p q r r"
[PROOF STATE]
proof (prove)
using this:
p \<noteq> q
r \<noteq> p
r \<noteq> q
proj2_set_Col {p, q, r}

goal (1 subgoal):
 1. cross_ratio_correct p q r r
[PROOF STEP]
by (unfold cross_ratio_correct_def) simp
[PROOF STATE]
proof (state)
this:
cross_ratio_correct p q r r

goal (1 subgoal):
 1. r = s
[PROOF STEP]
from \<open>proj2_set_Col {p,q,r}\<close>
[PROOF STATE]
proof (chain)
picking this:
proj2_set_Col {p, q, r}
[PROOF STEP]
have "proj2_Col p q r"
[PROOF STATE]
proof (prove)
using this:
proj2_set_Col {p, q, r}

goal (1 subgoal):
 1. proj2_Col p q r
[PROOF STEP]
by (subst proj2_Col_iff_set_Col)
[PROOF STATE]
proof (state)
this:
proj2_Col p q r

goal (1 subgoal):
 1. r = s
[PROOF STEP]
with \<open>p \<noteq> q\<close> and \<open>r \<noteq> p\<close> and \<open>r \<noteq> q\<close>
[PROOF STATE]
proof (chain)
picking this:
p \<noteq> q
r \<noteq> p
r \<noteq> q
proj2_Col p q r
[PROOF STEP]
have "cross_ratio p q r r = 1"
[PROOF STATE]
proof (prove)
using this:
p \<noteq> q
r \<noteq> p
r \<noteq> q
proj2_Col p q r

goal (1 subgoal):
 1. cross_ratio p q r r = 1
[PROOF STEP]
by (simp add: cross_ratio_equal_1)
[PROOF STATE]
proof (state)
this:
cross_ratio p q r r = 1

goal (1 subgoal):
 1. r = s
[PROOF STEP]
with \<open>cross_ratio p q r s = 1\<close>
[PROOF STATE]
proof (chain)
picking this:
cross_ratio p q r s = 1
cross_ratio p q r r = 1
[PROOF STEP]
have "cross_ratio p q r r = cross_ratio p q r s"
[PROOF STATE]
proof (prove)
using this:
cross_ratio p q r s = 1
cross_ratio p q r r = 1

goal (1 subgoal):
 1. cross_ratio p q r r = cross_ratio p q r s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cross_ratio p q r r = cross_ratio p q r s

goal (1 subgoal):
 1. r = s
[PROOF STEP]
with \<open>cross_ratio_correct p q r r\<close> and \<open>cross_ratio_correct p q r s\<close>
[PROOF STATE]
proof (chain)
picking this:
cross_ratio_correct p q r r
cross_ratio_correct p q r s
cross_ratio p q r r = cross_ratio p q r s
[PROOF STEP]
show "r = s"
[PROOF STATE]
proof (prove)
using this:
cross_ratio_correct p q r r
cross_ratio_correct p q r s
cross_ratio p q r r = cross_ratio p q r s

goal (1 subgoal):
 1. r = s
[PROOF STEP]
by (rule cross_ratio_unique)
[PROOF STATE]
proof (state)
this:
r = s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cross_ratio_swap_34:
  shows "cross_ratio p q s r = 1 / (cross_ratio p q r s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cross_ratio p q s r = 1 / cross_ratio p q r s
[PROOF STEP]
by (unfold cross_ratio_def) simp


[STATEMENT]
lemma cross_ratio_swap_13_24:
  assumes "cross_ratio_correct p q r s" and "r \<noteq> s"
  shows "cross_ratio r s p q = cross_ratio p q r s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cross_ratio r s p q = cross_ratio p q r s
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cross_ratio r s p q = cross_ratio p q r s
[PROOF STEP]
from \<open>cross_ratio_correct p q r s\<close>
[PROOF STATE]
proof (chain)
picking this:
cross_ratio_correct p q r s
[PROOF STEP]
have "proj2_set_Col {p,q,r,s}" and "p \<noteq> q" and "r \<noteq> p" and "s \<noteq> p" and "r \<noteq> q"
[PROOF STATE]
proof (prove)
using this:
cross_ratio_correct p q r s

goal (1 subgoal):
 1. (proj2_set_Col {p, q, r, s} &&& p \<noteq> q) &&& r \<noteq> p &&& s \<noteq> p &&& r \<noteq> q
[PROOF STEP]
by (unfold cross_ratio_correct_def, simp_all)
[PROOF STATE]
proof (state)
this:
proj2_set_Col {p, q, r, s}
p \<noteq> q
r \<noteq> p
s \<noteq> p
r \<noteq> q

goal (1 subgoal):
 1. cross_ratio r s p q = cross_ratio p q r s
[PROOF STEP]
have "proj2_rep p \<noteq> 0" (is "?u \<noteq> 0") and "proj2_rep q \<noteq> 0" (is "?v \<noteq> 0")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_rep p \<noteq> 0 &&& proj2_rep q \<noteq> 0
[PROOF STEP]
by (rule proj2_rep_non_zero)+
[PROOF STATE]
proof (state)
this:
proj2_rep p \<noteq> 0
proj2_rep q \<noteq> 0

goal (1 subgoal):
 1. cross_ratio r s p q = cross_ratio p q r s
[PROOF STEP]
have "p = proj2_abs ?u" and "q = proj2_abs ?v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p = proj2_abs (proj2_rep p) &&& q = proj2_abs (proj2_rep q)
[PROOF STEP]
by (simp_all add: proj2_abs_rep)
[PROOF STATE]
proof (state)
this:
p = proj2_abs (proj2_rep p)
q = proj2_abs (proj2_rep q)

goal (1 subgoal):
 1. cross_ratio r s p q = cross_ratio p q r s
[PROOF STEP]
with \<open>p \<noteq> q\<close>
[PROOF STATE]
proof (chain)
picking this:
p \<noteq> q
p = proj2_abs (proj2_rep p)
q = proj2_abs (proj2_rep q)
[PROOF STEP]
have "proj2_abs ?u \<noteq> proj2_abs ?v"
[PROOF STATE]
proof (prove)
using this:
p \<noteq> q
p = proj2_abs (proj2_rep p)
q = proj2_abs (proj2_rep q)

goal (1 subgoal):
 1. proj2_abs (proj2_rep p) \<noteq> proj2_abs (proj2_rep q)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
proj2_abs (proj2_rep p) \<noteq> proj2_abs (proj2_rep q)

goal (1 subgoal):
 1. cross_ratio r s p q = cross_ratio p q r s
[PROOF STEP]
let ?i = "proj2_Col_coeff p q r"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cross_ratio r s p q = cross_ratio p q r s
[PROOF STEP]
let ?j = "proj2_Col_coeff p q s"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cross_ratio r s p q = cross_ratio p q r s
[PROOF STEP]
from \<open>proj2_set_Col {p,q,r,s}\<close> and \<open>p \<noteq> q\<close> and \<open>r \<noteq> p\<close> and \<open>s \<noteq> p\<close>
[PROOF STATE]
proof (chain)
picking this:
proj2_set_Col {p, q, r, s}
p \<noteq> q
r \<noteq> p
s \<noteq> p
[PROOF STEP]
have "r = proj2_abs (?i *\<^sub>R ?u + ?v)" (is "r = proj2_abs ?w")
    and "s = proj2_abs (?j *\<^sub>R ?u + ?v)" (is "s = proj2_abs ?x")
[PROOF STATE]
proof (prove)
using this:
proj2_set_Col {p, q, r, s}
p \<noteq> q
r \<noteq> p
s \<noteq> p

goal (1 subgoal):
 1. r = proj2_abs (proj2_Col_coeff p q r *\<^sub>R proj2_rep p + proj2_rep q) &&& s = proj2_abs (proj2_Col_coeff p q s *\<^sub>R proj2_rep p + proj2_rep q)
[PROOF STEP]
by (simp_all add: proj2_set_Col_coeff)
[PROOF STATE]
proof (state)
this:
r = proj2_abs (proj2_Col_coeff p q r *\<^sub>R proj2_rep p + proj2_rep q)
s = proj2_abs (proj2_Col_coeff p q s *\<^sub>R proj2_rep p + proj2_rep q)

goal (1 subgoal):
 1. cross_ratio r s p q = cross_ratio p q r s
[PROOF STEP]
with \<open>r \<noteq> s\<close>
[PROOF STATE]
proof (chain)
picking this:
r \<noteq> s
r = proj2_abs (proj2_Col_coeff p q r *\<^sub>R proj2_rep p + proj2_rep q)
s = proj2_abs (proj2_Col_coeff p q s *\<^sub>R proj2_rep p + proj2_rep q)
[PROOF STEP]
have "?i \<noteq> ?j"
[PROOF STATE]
proof (prove)
using this:
r \<noteq> s
r = proj2_abs (proj2_Col_coeff p q r *\<^sub>R proj2_rep p + proj2_rep q)
s = proj2_abs (proj2_Col_coeff p q s *\<^sub>R proj2_rep p + proj2_rep q)

goal (1 subgoal):
 1. proj2_Col_coeff p q r \<noteq> proj2_Col_coeff p q s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
proj2_Col_coeff p q r \<noteq> proj2_Col_coeff p q s

goal (1 subgoal):
 1. cross_ratio r s p q = cross_ratio p q r s
[PROOF STEP]
from \<open>?u \<noteq> 0\<close> and \<open>?v \<noteq> 0\<close> and \<open>proj2_abs ?u \<noteq> proj2_abs ?v\<close>
    and dependent_proj2_abs [of ?u ?v _ 1]
[PROOF STATE]
proof (chain)
picking this:
proj2_rep p \<noteq> 0
proj2_rep q \<noteq> 0
proj2_abs (proj2_rep p) \<noteq> proj2_abs (proj2_rep q)
\<lbrakk>proj2_rep p \<noteq> 0; proj2_rep q \<noteq> 0; ?i \<noteq> 0 \<or> 1 \<noteq> 0; ?i *\<^sub>R proj2_rep p + 1 *\<^sub>R proj2_rep q = 0\<rbrakk> \<Longrightarrow> proj2_abs (proj2_rep p) = proj2_abs (proj2_rep q)
[PROOF STEP]
have "?w \<noteq> 0" and "?x \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
proj2_rep p \<noteq> 0
proj2_rep q \<noteq> 0
proj2_abs (proj2_rep p) \<noteq> proj2_abs (proj2_rep q)
\<lbrakk>proj2_rep p \<noteq> 0; proj2_rep q \<noteq> 0; ?i \<noteq> 0 \<or> 1 \<noteq> 0; ?i *\<^sub>R proj2_rep p + 1 *\<^sub>R proj2_rep q = 0\<rbrakk> \<Longrightarrow> proj2_abs (proj2_rep p) = proj2_abs (proj2_rep q)

goal (1 subgoal):
 1. proj2_Col_coeff p q r *\<^sub>R proj2_rep p + proj2_rep q \<noteq> 0 &&& proj2_Col_coeff p q s *\<^sub>R proj2_rep p + proj2_rep q \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
proj2_Col_coeff p q r *\<^sub>R proj2_rep p + proj2_rep q \<noteq> 0
proj2_Col_coeff p q s *\<^sub>R proj2_rep p + proj2_rep q \<noteq> 0

goal (1 subgoal):
 1. cross_ratio r s p q = cross_ratio p q r s
[PROOF STEP]
from \<open>r = proj2_abs (?i *\<^sub>R ?u + ?v)\<close> and \<open>r \<noteq> q\<close>
[PROOF STATE]
proof (chain)
picking this:
r = proj2_abs (proj2_Col_coeff p q r *\<^sub>R proj2_rep p + proj2_rep q)
r \<noteq> q
[PROOF STEP]
have "?i \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
r = proj2_abs (proj2_Col_coeff p q r *\<^sub>R proj2_rep p + proj2_rep q)
r \<noteq> q

goal (1 subgoal):
 1. proj2_Col_coeff p q r \<noteq> 0
[PROOF STEP]
by (auto simp add: proj2_abs_rep)
[PROOF STATE]
proof (state)
this:
proj2_Col_coeff p q r \<noteq> 0

goal (1 subgoal):
 1. cross_ratio r s p q = cross_ratio p q r s
[PROOF STEP]
have "?w - ?x = (?i - ?j) *\<^sub>R ?u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_Col_coeff p q r *\<^sub>R proj2_rep p + proj2_rep q - (proj2_Col_coeff p q s *\<^sub>R proj2_rep p + proj2_rep q) = (proj2_Col_coeff p q r - proj2_Col_coeff p q s) *\<^sub>R proj2_rep p
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
proj2_Col_coeff p q r *\<^sub>R proj2_rep p + proj2_rep q - (proj2_Col_coeff p q s *\<^sub>R proj2_rep p + proj2_rep q) = (proj2_Col_coeff p q r - proj2_Col_coeff p q s) *\<^sub>R proj2_rep p

goal (1 subgoal):
 1. cross_ratio r s p q = cross_ratio p q r s
[PROOF STEP]
with \<open>?i \<noteq> ?j\<close>
[PROOF STATE]
proof (chain)
picking this:
proj2_Col_coeff p q r \<noteq> proj2_Col_coeff p q s
proj2_Col_coeff p q r *\<^sub>R proj2_rep p + proj2_rep q - (proj2_Col_coeff p q s *\<^sub>R proj2_rep p + proj2_rep q) = (proj2_Col_coeff p q r - proj2_Col_coeff p q s) *\<^sub>R proj2_rep p
[PROOF STEP]
have "p = proj2_abs (?w - ?x)"
[PROOF STATE]
proof (prove)
using this:
proj2_Col_coeff p q r \<noteq> proj2_Col_coeff p q s
proj2_Col_coeff p q r *\<^sub>R proj2_rep p + proj2_rep q - (proj2_Col_coeff p q s *\<^sub>R proj2_rep p + proj2_rep q) = (proj2_Col_coeff p q r - proj2_Col_coeff p q s) *\<^sub>R proj2_rep p

goal (1 subgoal):
 1. p = proj2_abs (proj2_Col_coeff p q r *\<^sub>R proj2_rep p + proj2_rep q - (proj2_Col_coeff p q s *\<^sub>R proj2_rep p + proj2_rep q))
[PROOF STEP]
by (simp add: proj2_abs_mult_rep)
[PROOF STATE]
proof (state)
this:
p = proj2_abs (proj2_Col_coeff p q r *\<^sub>R proj2_rep p + proj2_rep q - (proj2_Col_coeff p q s *\<^sub>R proj2_rep p + proj2_rep q))

goal (1 subgoal):
 1. cross_ratio r s p q = cross_ratio p q r s
[PROOF STEP]
have "?j *\<^sub>R ?w - ?i *\<^sub>R ?x = (?j - ?i) *\<^sub>R ?v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_Col_coeff p q s *\<^sub>R (proj2_Col_coeff p q r *\<^sub>R proj2_rep p + proj2_rep q) - proj2_Col_coeff p q r *\<^sub>R (proj2_Col_coeff p q s *\<^sub>R proj2_rep p + proj2_rep q) = (proj2_Col_coeff p q s - proj2_Col_coeff p q r) *\<^sub>R proj2_rep q
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
proj2_Col_coeff p q s *\<^sub>R (proj2_Col_coeff p q r *\<^sub>R proj2_rep p + proj2_rep q) - proj2_Col_coeff p q r *\<^sub>R (proj2_Col_coeff p q s *\<^sub>R proj2_rep p + proj2_rep q) = (proj2_Col_coeff p q s - proj2_Col_coeff p q r) *\<^sub>R proj2_rep q

goal (1 subgoal):
 1. cross_ratio r s p q = cross_ratio p q r s
[PROOF STEP]
with \<open>?i \<noteq> ?j\<close>
[PROOF STATE]
proof (chain)
picking this:
proj2_Col_coeff p q r \<noteq> proj2_Col_coeff p q s
proj2_Col_coeff p q s *\<^sub>R (proj2_Col_coeff p q r *\<^sub>R proj2_rep p + proj2_rep q) - proj2_Col_coeff p q r *\<^sub>R (proj2_Col_coeff p q s *\<^sub>R proj2_rep p + proj2_rep q) = (proj2_Col_coeff p q s - proj2_Col_coeff p q r) *\<^sub>R proj2_rep q
[PROOF STEP]
have "q = proj2_abs (?j *\<^sub>R ?w - ?i *\<^sub>R ?x)"
[PROOF STATE]
proof (prove)
using this:
proj2_Col_coeff p q r \<noteq> proj2_Col_coeff p q s
proj2_Col_coeff p q s *\<^sub>R (proj2_Col_coeff p q r *\<^sub>R proj2_rep p + proj2_rep q) - proj2_Col_coeff p q r *\<^sub>R (proj2_Col_coeff p q s *\<^sub>R proj2_rep p + proj2_rep q) = (proj2_Col_coeff p q s - proj2_Col_coeff p q r) *\<^sub>R proj2_rep q

goal (1 subgoal):
 1. q = proj2_abs (proj2_Col_coeff p q s *\<^sub>R (proj2_Col_coeff p q r *\<^sub>R proj2_rep p + proj2_rep q) - proj2_Col_coeff p q r *\<^sub>R (proj2_Col_coeff p q s *\<^sub>R proj2_rep p + proj2_rep q))
[PROOF STEP]
by (simp add: proj2_abs_mult_rep)
[PROOF STATE]
proof (state)
this:
q = proj2_abs (proj2_Col_coeff p q s *\<^sub>R (proj2_Col_coeff p q r *\<^sub>R proj2_rep p + proj2_rep q) - proj2_Col_coeff p q r *\<^sub>R (proj2_Col_coeff p q s *\<^sub>R proj2_rep p + proj2_rep q))

goal (1 subgoal):
 1. cross_ratio r s p q = cross_ratio p q r s
[PROOF STEP]
with \<open>?w \<noteq> 0\<close> and \<open>?x \<noteq> 0\<close> and \<open>r \<noteq> s\<close> and \<open>?i \<noteq> 0\<close> and \<open>r = proj2_abs ?w\<close>
    and \<open>s = proj2_abs ?x\<close> and \<open>p = proj2_abs (?w - ?x)\<close>
    and cross_ratio_abs [of ?w ?x "-1" "-?i" 1 ?j]
[PROOF STATE]
proof (chain)
picking this:
proj2_Col_coeff p q r *\<^sub>R proj2_rep p + proj2_rep q \<noteq> 0
proj2_Col_coeff p q s *\<^sub>R proj2_rep p + proj2_rep q \<noteq> 0
r \<noteq> s
proj2_Col_coeff p q r \<noteq> 0
r = proj2_abs (proj2_Col_coeff p q r *\<^sub>R proj2_rep p + proj2_rep q)
s = proj2_abs (proj2_Col_coeff p q s *\<^sub>R proj2_rep p + proj2_rep q)
p = proj2_abs (proj2_Col_coeff p q r *\<^sub>R proj2_rep p + proj2_rep q - (proj2_Col_coeff p q s *\<^sub>R proj2_rep p + proj2_rep q))
\<lbrakk>proj2_Col_coeff p q r *\<^sub>R proj2_rep p + proj2_rep q \<noteq> 0; proj2_Col_coeff p q s *\<^sub>R proj2_rep p + proj2_rep q \<noteq> 0; proj2_abs (proj2_Col_coeff p q r *\<^sub>R proj2_rep p + proj2_rep q) \<noteq> proj2_abs (proj2_Col_coeff p q s *\<^sub>R proj2_rep p + proj2_rep q); - 1 \<noteq> 0; - proj2_Col_coeff p q r \<noteq> 0\<rbrakk> \<Longrightarrow> cross_ratio (proj2_abs (proj2_Col_coeff p q r *\<^sub>R proj2_rep p + proj2_rep q)) (proj2_abs (proj2_Col_coeff p q s *\<^sub>R proj2_rep p + proj2_rep q)) (proj2_abs (1 *\<^sub>R (proj2_Col_coeff p q r *\<^sub>R proj2_rep p + proj2_rep q) + - 1 *\<^sub>R (proj2_Col_coeff p q s *\<^sub>R proj2_rep p + proj2_rep q))) (proj2_abs (proj2_Col_coeff p q s *\<^sub>R (proj2_Col_coeff p q r *\<^sub>R proj2_rep p + proj2_rep q) + - proj2_Col_coeff p q r *\<^sub>R (proj2_Col_coeff p q s *\<^sub>R proj2_rep p + proj2_rep q))) = - 1 * proj2_Col_coeff p q s / (1 * - proj2_Col_coeff p q r)
q = proj2_abs (proj2_Col_coeff p q s *\<^sub>R (proj2_Col_coeff p q r *\<^sub>R proj2_rep p + proj2_rep q) - proj2_Col_coeff p q r *\<^sub>R (proj2_Col_coeff p q s *\<^sub>R proj2_rep p + proj2_rep q))
[PROOF STEP]
have "cross_ratio r s p q = ?j / ?i"
[PROOF STATE]
proof (prove)
using this:
proj2_Col_coeff p q r *\<^sub>R proj2_rep p + proj2_rep q \<noteq> 0
proj2_Col_coeff p q s *\<^sub>R proj2_rep p + proj2_rep q \<noteq> 0
r \<noteq> s
proj2_Col_coeff p q r \<noteq> 0
r = proj2_abs (proj2_Col_coeff p q r *\<^sub>R proj2_rep p + proj2_rep q)
s = proj2_abs (proj2_Col_coeff p q s *\<^sub>R proj2_rep p + proj2_rep q)
p = proj2_abs (proj2_Col_coeff p q r *\<^sub>R proj2_rep p + proj2_rep q - (proj2_Col_coeff p q s *\<^sub>R proj2_rep p + proj2_rep q))
\<lbrakk>proj2_Col_coeff p q r *\<^sub>R proj2_rep p + proj2_rep q \<noteq> 0; proj2_Col_coeff p q s *\<^sub>R proj2_rep p + proj2_rep q \<noteq> 0; proj2_abs (proj2_Col_coeff p q r *\<^sub>R proj2_rep p + proj2_rep q) \<noteq> proj2_abs (proj2_Col_coeff p q s *\<^sub>R proj2_rep p + proj2_rep q); - 1 \<noteq> 0; - proj2_Col_coeff p q r \<noteq> 0\<rbrakk> \<Longrightarrow> cross_ratio (proj2_abs (proj2_Col_coeff p q r *\<^sub>R proj2_rep p + proj2_rep q)) (proj2_abs (proj2_Col_coeff p q s *\<^sub>R proj2_rep p + proj2_rep q)) (proj2_abs (1 *\<^sub>R (proj2_Col_coeff p q r *\<^sub>R proj2_rep p + proj2_rep q) + - 1 *\<^sub>R (proj2_Col_coeff p q s *\<^sub>R proj2_rep p + proj2_rep q))) (proj2_abs (proj2_Col_coeff p q s *\<^sub>R (proj2_Col_coeff p q r *\<^sub>R proj2_rep p + proj2_rep q) + - proj2_Col_coeff p q r *\<^sub>R (proj2_Col_coeff p q s *\<^sub>R proj2_rep p + proj2_rep q))) = - 1 * proj2_Col_coeff p q s / (1 * - proj2_Col_coeff p q r)
q = proj2_abs (proj2_Col_coeff p q s *\<^sub>R (proj2_Col_coeff p q r *\<^sub>R proj2_rep p + proj2_rep q) - proj2_Col_coeff p q r *\<^sub>R (proj2_Col_coeff p q s *\<^sub>R proj2_rep p + proj2_rep q))

goal (1 subgoal):
 1. cross_ratio r s p q = proj2_Col_coeff p q s / proj2_Col_coeff p q r
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
cross_ratio r s p q = proj2_Col_coeff p q s / proj2_Col_coeff p q r

goal (1 subgoal):
 1. cross_ratio r s p q = cross_ratio p q r s
[PROOF STEP]
thus "cross_ratio r s p q = cross_ratio p q r s"
[PROOF STATE]
proof (prove)
using this:
cross_ratio r s p q = proj2_Col_coeff p q s / proj2_Col_coeff p q r

goal (1 subgoal):
 1. cross_ratio r s p q = cross_ratio p q r s
[PROOF STEP]
by (unfold cross_ratio_def [of p q r s], simp)
[PROOF STATE]
proof (state)
this:
cross_ratio r s p q = cross_ratio p q r s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cross_ratio_swap_12:
  assumes "cross_ratio_correct p q r s" and "cross_ratio_correct q p r s"
  shows "cross_ratio q p r s = 1 / (cross_ratio p q r s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cross_ratio q p r s = 1 / cross_ratio p q r s
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> cross_ratio q p r s = 1 / cross_ratio p q r s
 2. \<not> ?P \<Longrightarrow> cross_ratio q p r s = 1 / cross_ratio p q r s
[PROOF STEP]
assume "r = s"
[PROOF STATE]
proof (state)
this:
r = s

goal (2 subgoals):
 1. ?P \<Longrightarrow> cross_ratio q p r s = 1 / cross_ratio p q r s
 2. \<not> ?P \<Longrightarrow> cross_ratio q p r s = 1 / cross_ratio p q r s
[PROOF STEP]
from \<open>cross_ratio_correct p q r s\<close>
[PROOF STATE]
proof (chain)
picking this:
cross_ratio_correct p q r s
[PROOF STEP]
have "proj2_set_Col {p,q,r,s}" and "p \<noteq> q" and "r \<noteq> p" and "r \<noteq> q"
[PROOF STATE]
proof (prove)
using this:
cross_ratio_correct p q r s

goal (1 subgoal):
 1. (proj2_set_Col {p, q, r, s} &&& p \<noteq> q) &&& r \<noteq> p &&& r \<noteq> q
[PROOF STEP]
by (unfold cross_ratio_correct_def) simp_all
[PROOF STATE]
proof (state)
this:
proj2_set_Col {p, q, r, s}
p \<noteq> q
r \<noteq> p
r \<noteq> q

goal (2 subgoals):
 1. ?P \<Longrightarrow> cross_ratio q p r s = 1 / cross_ratio p q r s
 2. \<not> ?P \<Longrightarrow> cross_ratio q p r s = 1 / cross_ratio p q r s
[PROOF STEP]
from \<open>proj2_set_Col {p,q,r,s}\<close> and \<open>r = s\<close>
[PROOF STATE]
proof (chain)
picking this:
proj2_set_Col {p, q, r, s}
r = s
[PROOF STEP]
have "proj2_Col p q r"
[PROOF STATE]
proof (prove)
using this:
proj2_set_Col {p, q, r, s}
r = s

goal (1 subgoal):
 1. proj2_Col p q r
[PROOF STEP]
by (simp_all add: proj2_Col_iff_set_Col)
[PROOF STATE]
proof (state)
this:
proj2_Col p q r

goal (2 subgoals):
 1. ?P \<Longrightarrow> cross_ratio q p r s = 1 / cross_ratio p q r s
 2. \<not> ?P \<Longrightarrow> cross_ratio q p r s = 1 / cross_ratio p q r s
[PROOF STEP]
hence "proj2_Col q p r"
[PROOF STATE]
proof (prove)
using this:
proj2_Col p q r

goal (1 subgoal):
 1. proj2_Col q p r
[PROOF STEP]
by (rule proj2_Col_permute)
[PROOF STATE]
proof (state)
this:
proj2_Col q p r

goal (2 subgoals):
 1. ?P \<Longrightarrow> cross_ratio q p r s = 1 / cross_ratio p q r s
 2. \<not> ?P \<Longrightarrow> cross_ratio q p r s = 1 / cross_ratio p q r s
[PROOF STEP]
with \<open>proj2_Col p q r\<close> and \<open>p \<noteq> q\<close> and \<open>r \<noteq> p\<close> and \<open>r \<noteq> q\<close> and \<open>r = s\<close>
[PROOF STATE]
proof (chain)
picking this:
proj2_Col p q r
p \<noteq> q
r \<noteq> p
r \<noteq> q
r = s
proj2_Col q p r
[PROOF STEP]
have "cross_ratio p q r s = 1" and "cross_ratio q p r s = 1"
[PROOF STATE]
proof (prove)
using this:
proj2_Col p q r
p \<noteq> q
r \<noteq> p
r \<noteq> q
r = s
proj2_Col q p r

goal (1 subgoal):
 1. cross_ratio p q r s = 1 &&& cross_ratio q p r s = 1
[PROOF STEP]
by (simp_all add: cross_ratio_equal_1)
[PROOF STATE]
proof (state)
this:
cross_ratio p q r s = 1
cross_ratio q p r s = 1

goal (2 subgoals):
 1. ?P \<Longrightarrow> cross_ratio q p r s = 1 / cross_ratio p q r s
 2. \<not> ?P \<Longrightarrow> cross_ratio q p r s = 1 / cross_ratio p q r s
[PROOF STEP]
thus "cross_ratio q p r s = 1 / (cross_ratio p q r s)"
[PROOF STATE]
proof (prove)
using this:
cross_ratio p q r s = 1
cross_ratio q p r s = 1

goal (1 subgoal):
 1. cross_ratio q p r s = 1 / cross_ratio p q r s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cross_ratio q p r s = 1 / cross_ratio p q r s

goal (1 subgoal):
 1. r \<noteq> s \<Longrightarrow> cross_ratio q p r s = 1 / cross_ratio p q r s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. r \<noteq> s \<Longrightarrow> cross_ratio q p r s = 1 / cross_ratio p q r s
[PROOF STEP]
assume "r \<noteq> s"
[PROOF STATE]
proof (state)
this:
r \<noteq> s

goal (1 subgoal):
 1. r \<noteq> s \<Longrightarrow> cross_ratio q p r s = 1 / cross_ratio p q r s
[PROOF STEP]
with \<open>cross_ratio_correct q p r s\<close>
[PROOF STATE]
proof (chain)
picking this:
cross_ratio_correct q p r s
r \<noteq> s
[PROOF STEP]
have "cross_ratio q p r s = cross_ratio r s q p"
[PROOF STATE]
proof (prove)
using this:
cross_ratio_correct q p r s
r \<noteq> s

goal (1 subgoal):
 1. cross_ratio q p r s = cross_ratio r s q p
[PROOF STEP]
by (simp add: cross_ratio_swap_13_24)
[PROOF STATE]
proof (state)
this:
cross_ratio q p r s = cross_ratio r s q p

goal (1 subgoal):
 1. r \<noteq> s \<Longrightarrow> cross_ratio q p r s = 1 / cross_ratio p q r s
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cross_ratio q p r s = cross_ratio r s q p

goal (1 subgoal):
 1. r \<noteq> s \<Longrightarrow> cross_ratio q p r s = 1 / cross_ratio p q r s
[PROOF STEP]
have "\<dots> = 1 / (cross_ratio r s p q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cross_ratio r s q p = 1 / cross_ratio r s p q
[PROOF STEP]
by (rule cross_ratio_swap_34)
[PROOF STATE]
proof (state)
this:
cross_ratio r s q p = 1 / cross_ratio r s p q

goal (1 subgoal):
 1. r \<noteq> s \<Longrightarrow> cross_ratio q p r s = 1 / cross_ratio p q r s
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cross_ratio r s q p = 1 / cross_ratio r s p q

goal (1 subgoal):
 1. r \<noteq> s \<Longrightarrow> cross_ratio q p r s = 1 / cross_ratio p q r s
[PROOF STEP]
from \<open>cross_ratio_correct p q r s\<close> and \<open>r \<noteq> s\<close>
[PROOF STATE]
proof (chain)
picking this:
cross_ratio_correct p q r s
r \<noteq> s
[PROOF STEP]
have "\<dots> = 1 / (cross_ratio p q r s)"
[PROOF STATE]
proof (prove)
using this:
cross_ratio_correct p q r s
r \<noteq> s

goal (1 subgoal):
 1. 1 / cross_ratio r s p q = 1 / cross_ratio p q r s
[PROOF STEP]
by (simp add: cross_ratio_swap_13_24)
[PROOF STATE]
proof (state)
this:
1 / cross_ratio r s p q = 1 / cross_ratio p q r s

goal (1 subgoal):
 1. r \<noteq> s \<Longrightarrow> cross_ratio q p r s = 1 / cross_ratio p q r s
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
cross_ratio q p r s = 1 / cross_ratio p q r s
[PROOF STEP]
show "cross_ratio q p r s = 1 / (cross_ratio p q r s)"
[PROOF STATE]
proof (prove)
using this:
cross_ratio q p r s = 1 / cross_ratio p q r s

goal (1 subgoal):
 1. cross_ratio q p r s = 1 / cross_ratio p q r s
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
cross_ratio q p r s = 1 / cross_ratio p q r s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vector2_append1_non_zero: "vector2_append1 v \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector2_append1 v \<noteq> 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vector2_append1 v \<noteq> 0
[PROOF STEP]
have "(vector2_append1 v)$3 \<noteq> 0$3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector2_append1 v $ 3 \<noteq> 0 $ (3::'a)
[PROOF STEP]
unfolding vector2_append1_def and vector_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_lambda (foldr (\<lambda>x f n. (f (n + 1))(n := x)) [v $ 1, v $ 2, 1] (\<lambda>n x. 0) 1) $ 3 \<noteq> 0 $ (3::'a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vector2_append1 v $ 3 \<noteq> 0 $ (3::?'a1)

goal (1 subgoal):
 1. vector2_append1 v \<noteq> 0
[PROOF STEP]
thus "vector2_append1 v \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
vector2_append1 v $ 3 \<noteq> 0 $ (3::?'a1)

goal (1 subgoal):
 1. vector2_append1 v \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vector2_append1 v \<noteq> 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proj2_pt_scalar:
  "\<exists> c. c \<noteq> 0 \<and> proj2_rep (proj2_pt v) = c *\<^sub>R vector2_append1 v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>c. c \<noteq> 0 \<and> proj2_rep (proj2_pt v) = c *\<^sub>R vector2_append1 v
[PROOF STEP]
unfolding proj2_pt_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>c. c \<noteq> 0 \<and> proj2_rep (proj2_abs (vector2_append1 v)) = c *\<^sub>R vector2_append1 v
[PROOF STEP]
by (simp add: proj2_rep_abs2 vector2_append1_non_zero)


[STATEMENT]
lemma cart2_append1_z:
  assumes "z_non_zero p"
  shows "(cart2_append1 p)$3 = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cart2_append1 p $ 3 = 1
[PROOF STEP]
using \<open>z_non_zero p\<close>
[PROOF STATE]
proof (prove)
using this:
z_non_zero p

goal (1 subgoal):
 1. cart2_append1 p $ 3 = 1
[PROOF STEP]
by (unfold cart2_append1_def) simp


[STATEMENT]
lemma cart2_append1_non_zero:
  assumes "z_non_zero p"
  shows "cart2_append1 p \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cart2_append1 p \<noteq> 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cart2_append1 p \<noteq> 0
[PROOF STEP]
from \<open>z_non_zero p\<close>
[PROOF STATE]
proof (chain)
picking this:
z_non_zero p
[PROOF STEP]
have "(cart2_append1 p)$3 = 1"
[PROOF STATE]
proof (prove)
using this:
z_non_zero p

goal (1 subgoal):
 1. cart2_append1 p $ 3 = 1
[PROOF STEP]
by (rule cart2_append1_z)
[PROOF STATE]
proof (state)
this:
cart2_append1 p $ 3 = 1

goal (1 subgoal):
 1. cart2_append1 p \<noteq> 0
[PROOF STEP]
thus "cart2_append1 p \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
cart2_append1 p $ 3 = 1

goal (1 subgoal):
 1. cart2_append1 p \<noteq> 0
[PROOF STEP]
by (simp add: vec_eq_iff exI [of _ 3])
[PROOF STATE]
proof (state)
this:
cart2_append1 p \<noteq> 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proj2_rep_cart2_append1:
  assumes "z_non_zero p"
  shows "proj2_rep p = ((proj2_rep p)$3) *\<^sub>R cart2_append1 p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_rep p = proj2_rep p $ 3 *\<^sub>R cart2_append1 p
[PROOF STEP]
using \<open>z_non_zero p\<close>
[PROOF STATE]
proof (prove)
using this:
z_non_zero p

goal (1 subgoal):
 1. proj2_rep p = proj2_rep p $ 3 *\<^sub>R cart2_append1 p
[PROOF STEP]
by (unfold cart2_append1_def) simp


[STATEMENT]
lemma proj2_abs_cart2_append1:
  assumes "z_non_zero p"
  shows "proj2_abs (cart2_append1 p) = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_abs (cart2_append1 p) = p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. proj2_abs (cart2_append1 p) = p
[PROOF STEP]
from \<open>z_non_zero p\<close>
[PROOF STATE]
proof (chain)
picking this:
z_non_zero p
[PROOF STEP]
have "proj2_abs (cart2_append1 p) = proj2_abs (proj2_rep p)"
[PROOF STATE]
proof (prove)
using this:
z_non_zero p

goal (1 subgoal):
 1. proj2_abs (cart2_append1 p) = proj2_abs (proj2_rep p)
[PROOF STEP]
by (unfold cart2_append1_def) (simp add: proj2_abs_mult)
[PROOF STATE]
proof (state)
this:
proj2_abs (cart2_append1 p) = proj2_abs (proj2_rep p)

goal (1 subgoal):
 1. proj2_abs (cart2_append1 p) = p
[PROOF STEP]
thus "proj2_abs (cart2_append1 p) = p"
[PROOF STATE]
proof (prove)
using this:
proj2_abs (cart2_append1 p) = proj2_abs (proj2_rep p)

goal (1 subgoal):
 1. proj2_abs (cart2_append1 p) = p
[PROOF STEP]
by (simp add: proj2_abs_rep)
[PROOF STATE]
proof (state)
this:
proj2_abs (cart2_append1 p) = p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cart2_append1_inj:
  assumes "z_non_zero p" and "cart2_append1 p = cart2_append1 q"
  shows "p = q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p = q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p = q
[PROOF STEP]
from \<open>z_non_zero p\<close>
[PROOF STATE]
proof (chain)
picking this:
z_non_zero p
[PROOF STEP]
have "(cart2_append1 p)$3 = 1"
[PROOF STATE]
proof (prove)
using this:
z_non_zero p

goal (1 subgoal):
 1. cart2_append1 p $ 3 = 1
[PROOF STEP]
by (rule cart2_append1_z)
[PROOF STATE]
proof (state)
this:
cart2_append1 p $ 3 = 1

goal (1 subgoal):
 1. p = q
[PROOF STEP]
with \<open>cart2_append1 p = cart2_append1 q\<close>
[PROOF STATE]
proof (chain)
picking this:
cart2_append1 p = cart2_append1 q
cart2_append1 p $ 3 = 1
[PROOF STEP]
have "(cart2_append1 q)$3 = 1"
[PROOF STATE]
proof (prove)
using this:
cart2_append1 p = cart2_append1 q
cart2_append1 p $ 3 = 1

goal (1 subgoal):
 1. cart2_append1 q $ 3 = 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cart2_append1 q $ 3 = 1

goal (1 subgoal):
 1. p = q
[PROOF STEP]
hence "z_non_zero q"
[PROOF STATE]
proof (prove)
using this:
cart2_append1 q $ 3 = 1

goal (1 subgoal):
 1. z_non_zero q
[PROOF STEP]
by (unfold cart2_append1_def) auto
[PROOF STATE]
proof (state)
this:
z_non_zero q

goal (1 subgoal):
 1. p = q
[PROOF STEP]
from \<open>cart2_append1 p = cart2_append1 q\<close>
[PROOF STATE]
proof (chain)
picking this:
cart2_append1 p = cart2_append1 q
[PROOF STEP]
have "proj2_abs (cart2_append1 p) = proj2_abs (cart2_append1 q)"
[PROOF STATE]
proof (prove)
using this:
cart2_append1 p = cart2_append1 q

goal (1 subgoal):
 1. proj2_abs (cart2_append1 p) = proj2_abs (cart2_append1 q)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
proj2_abs (cart2_append1 p) = proj2_abs (cart2_append1 q)

goal (1 subgoal):
 1. p = q
[PROOF STEP]
with \<open>z_non_zero p\<close> and \<open>z_non_zero q\<close>
[PROOF STATE]
proof (chain)
picking this:
z_non_zero p
z_non_zero q
proj2_abs (cart2_append1 p) = proj2_abs (cart2_append1 q)
[PROOF STEP]
show "p = q"
[PROOF STATE]
proof (prove)
using this:
z_non_zero p
z_non_zero q
proj2_abs (cart2_append1 p) = proj2_abs (cart2_append1 q)

goal (1 subgoal):
 1. p = q
[PROOF STEP]
by (simp add: proj2_abs_cart2_append1)
[PROOF STATE]
proof (state)
this:
p = q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cart2_append1:
  assumes "z_non_zero p"
  shows "vector2_append1 (cart2_pt p) = cart2_append1 p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector2_append1 (cart2_pt p) = cart2_append1 p
[PROOF STEP]
using \<open>z_non_zero p\<close>
[PROOF STATE]
proof (prove)
using this:
z_non_zero p

goal (1 subgoal):
 1. vector2_append1 (cart2_pt p) = cart2_append1 p
[PROOF STEP]
unfolding vector2_append1_def
    and cart2_append1_def
    and cart2_pt_def
    and vector_def
[PROOF STATE]
proof (prove)
using this:
z_non_zero p

goal (1 subgoal):
 1. vec_lambda (foldr (\<lambda>x f n. (f (n + 1))(n := x)) [vec_lambda (foldr (\<lambda>x f n. (f (n + 1))(n := x)) [proj2_rep p $ 1 / proj2_rep p $ 3, proj2_rep p $ 2 / proj2_rep p $ 3] (\<lambda>n x. 0) 1) $ 1, vec_lambda (foldr (\<lambda>x f n. (f (n + 1))(n := x)) [proj2_rep p $ 1 / proj2_rep p $ 3, proj2_rep p $ 2 / proj2_rep p $ 3] (\<lambda>n x. 0) 1) $ 2, 1] (\<lambda>n x. 0) 1) = (1 / proj2_rep p $ 3) *\<^sub>R proj2_rep p
[PROOF STEP]
by (simp add: vec_eq_iff forall_3)


[STATEMENT]
lemma cart2_proj2: "cart2_pt (proj2_pt v) = v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cart2_pt (proj2_pt v) = v
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cart2_pt (proj2_pt v) = v
[PROOF STEP]
let ?v' = "vector2_append1 v"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cart2_pt (proj2_pt v) = v
[PROOF STEP]
let ?p = "proj2_pt v"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cart2_pt (proj2_pt v) = v
[PROOF STEP]
from proj2_pt_scalar
[PROOF STATE]
proof (chain)
picking this:
\<exists>c. c \<noteq> 0 \<and> proj2_rep (proj2_pt ?v) = c *\<^sub>R vector2_append1 ?v
[PROOF STEP]
obtain c where "c \<noteq> 0" and "proj2_rep ?p = c *\<^sub>R ?v'"
[PROOF STATE]
proof (prove)
using this:
\<exists>c. c \<noteq> 0 \<and> proj2_rep (proj2_pt ?v) = c *\<^sub>R vector2_append1 ?v

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>c \<noteq> 0; proj2_rep (proj2_pt v) = c *\<^sub>R vector2_append1 v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c \<noteq> 0
proj2_rep (proj2_pt v) = c *\<^sub>R vector2_append1 v

goal (1 subgoal):
 1. cart2_pt (proj2_pt v) = v
[PROOF STEP]
hence "(cart2_pt ?p)$1 = v$1" and "(cart2_pt ?p)$2 = v$2"
[PROOF STATE]
proof (prove)
using this:
c \<noteq> 0
proj2_rep (proj2_pt v) = c *\<^sub>R vector2_append1 v

goal (1 subgoal):
 1. cart2_pt (proj2_pt v) $ 1 = v $ 1 &&& cart2_pt (proj2_pt v) $ 2 = v $ 2
[PROOF STEP]
unfolding cart2_pt_def and vector2_append1_def and vector_def
[PROOF STATE]
proof (prove)
using this:
c \<noteq> 0
proj2_rep (proj2_pt v) = c *\<^sub>R vec_lambda (foldr (\<lambda>x f n. (f (n + 1))(n := x)) [v $ 1, v $ 2, 1] (\<lambda>n x. 0) 1)

goal (1 subgoal):
 1. vec_lambda (foldr (\<lambda>x f n. (f (n + 1))(n := x)) [proj2_rep (proj2_pt v) $ 1 / proj2_rep (proj2_pt v) $ 3, proj2_rep (proj2_pt v) $ 2 / proj2_rep (proj2_pt v) $ 3] (\<lambda>n x. 0) 1) $ 1 = v $ 1 &&& vec_lambda (foldr (\<lambda>x f n. (f (n + 1))(n := x)) [proj2_rep (proj2_pt v) $ 1 / proj2_rep (proj2_pt v) $ 3, proj2_rep (proj2_pt v) $ 2 / proj2_rep (proj2_pt v) $ 3] (\<lambda>n x. 0) 1) $ 2 = v $ 2
[PROOF STEP]
by simp+
[PROOF STATE]
proof (state)
this:
cart2_pt (proj2_pt v) $ 1 = v $ 1
cart2_pt (proj2_pt v) $ 2 = v $ 2

goal (1 subgoal):
 1. cart2_pt (proj2_pt v) = v
[PROOF STEP]
thus "cart2_pt ?p = v"
[PROOF STATE]
proof (prove)
using this:
cart2_pt (proj2_pt v) $ 1 = v $ 1
cart2_pt (proj2_pt v) $ 2 = v $ 2

goal (1 subgoal):
 1. cart2_pt (proj2_pt v) = v
[PROOF STEP]
by (simp add: vec_eq_iff forall_2)
[PROOF STATE]
proof (state)
this:
cart2_pt (proj2_pt v) = v

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma z_non_zero_proj2_pt: "z_non_zero (proj2_pt v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z_non_zero (proj2_pt v)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. z_non_zero (proj2_pt v)
[PROOF STEP]
from proj2_pt_scalar
[PROOF STATE]
proof (chain)
picking this:
\<exists>c. c \<noteq> 0 \<and> proj2_rep (proj2_pt ?v) = c *\<^sub>R vector2_append1 ?v
[PROOF STEP]
obtain c where "c \<noteq> 0" and "proj2_rep (proj2_pt v) = c *\<^sub>R (vector2_append1 v)"
[PROOF STATE]
proof (prove)
using this:
\<exists>c. c \<noteq> 0 \<and> proj2_rep (proj2_pt ?v) = c *\<^sub>R vector2_append1 ?v

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>c \<noteq> 0; proj2_rep (proj2_pt v) = c *\<^sub>R vector2_append1 v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c \<noteq> 0
proj2_rep (proj2_pt v) = c *\<^sub>R vector2_append1 v

goal (1 subgoal):
 1. z_non_zero (proj2_pt v)
[PROOF STEP]
from \<open>proj2_rep (proj2_pt v) = c *\<^sub>R (vector2_append1 v)\<close>
[PROOF STATE]
proof (chain)
picking this:
proj2_rep (proj2_pt v) = c *\<^sub>R vector2_append1 v
[PROOF STEP]
have "(proj2_rep (proj2_pt v))$3 = c"
[PROOF STATE]
proof (prove)
using this:
proj2_rep (proj2_pt v) = c *\<^sub>R vector2_append1 v

goal (1 subgoal):
 1. proj2_rep (proj2_pt v) $ 3 = c
[PROOF STEP]
unfolding vector2_append1_def and vector_def
[PROOF STATE]
proof (prove)
using this:
proj2_rep (proj2_pt v) = c *\<^sub>R vec_lambda (foldr (\<lambda>x f n. (f (n + 1))(n := x)) [v $ 1, v $ 2, 1] (\<lambda>n x. 0) 1)

goal (1 subgoal):
 1. proj2_rep (proj2_pt v) $ 3 = c
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
proj2_rep (proj2_pt v) $ 3 = c

goal (1 subgoal):
 1. z_non_zero (proj2_pt v)
[PROOF STEP]
with \<open>c \<noteq> 0\<close>
[PROOF STATE]
proof (chain)
picking this:
c \<noteq> 0
proj2_rep (proj2_pt v) $ 3 = c
[PROOF STEP]
show "z_non_zero (proj2_pt v)"
[PROOF STATE]
proof (prove)
using this:
c \<noteq> 0
proj2_rep (proj2_pt v) $ 3 = c

goal (1 subgoal):
 1. z_non_zero (proj2_pt v)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
z_non_zero (proj2_pt v)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cart2_append1_proj2: "cart2_append1 (proj2_pt v) = vector2_append1 v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cart2_append1 (proj2_pt v) = vector2_append1 v
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cart2_append1 (proj2_pt v) = vector2_append1 v
[PROOF STEP]
from z_non_zero_proj2_pt
[PROOF STATE]
proof (chain)
picking this:
z_non_zero (proj2_pt ?v)
[PROOF STEP]
have "cart2_append1 (proj2_pt v) = vector2_append1 (cart2_pt (proj2_pt v))"
[PROOF STATE]
proof (prove)
using this:
z_non_zero (proj2_pt ?v)

goal (1 subgoal):
 1. cart2_append1 (proj2_pt v) = vector2_append1 (cart2_pt (proj2_pt v))
[PROOF STEP]
by (simp add: cart2_append1)
[PROOF STATE]
proof (state)
this:
cart2_append1 (proj2_pt v) = vector2_append1 (cart2_pt (proj2_pt v))

goal (1 subgoal):
 1. cart2_append1 (proj2_pt v) = vector2_append1 v
[PROOF STEP]
thus "cart2_append1 (proj2_pt v) = vector2_append1 v"
[PROOF STATE]
proof (prove)
using this:
cart2_append1 (proj2_pt v) = vector2_append1 (cart2_pt (proj2_pt v))

goal (1 subgoal):
 1. cart2_append1 (proj2_pt v) = vector2_append1 v
[PROOF STEP]
by (simp add: cart2_proj2)
[PROOF STATE]
proof (state)
this:
cart2_append1 (proj2_pt v) = vector2_append1 v

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proj2_pt_inj: "inj proj2_pt"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj proj2_pt
[PROOF STEP]
by (simp add: inj_on_inverseI [of UNIV cart2_pt proj2_pt] cart2_proj2)


[STATEMENT]
lemma proj2_cart2:
  assumes "z_non_zero p"
  shows "proj2_pt (cart2_pt p) = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj2_pt (cart2_pt p) = p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. proj2_pt (cart2_pt p) = p
[PROOF STEP]
from \<open>z_non_zero p\<close>
[PROOF STATE]
proof (chain)
picking this:
z_non_zero p
[PROOF STEP]
have "(proj2_rep p)$3 *\<^sub>R vector2_append1 (cart2_pt p) = proj2_rep p"
[PROOF STATE]
proof (prove)
using this:
z_non_zero p

goal (1 subgoal):
 1. proj2_rep p $ 3 *\<^sub>R vector2_append1 (cart2_pt p) = proj2_rep p
[PROOF STEP]
unfolding vector2_append1_def and cart2_pt_def and vector_def
[PROOF STATE]
proof (prove)
using this:
z_non_zero p

goal (1 subgoal):
 1. proj2_rep p $ 3 *\<^sub>R vec_lambda (foldr (\<lambda>x f n. (f (n + 1))(n := x)) [vec_lambda (foldr (\<lambda>x f n. (f (n + 1))(n := x)) [proj2_rep p $ 1 / proj2_rep p $ 3, proj2_rep p $ 2 / proj2_rep p $ 3] (\<lambda>n x. 0) 1) $ 1, vec_lambda (foldr (\<lambda>x f n. (f (n + 1))(n := x)) [proj2_rep p $ 1 / proj2_rep p $ 3, proj2_rep p $ 2 / proj2_rep p $ 3] (\<lambda>n x. 0) 1) $ 2, 1] (\<lambda>n x. 0) 1) = proj2_rep p
[PROOF STEP]
by (simp add: vec_eq_iff forall_3)
[PROOF STATE]
proof (state)
this:
proj2_rep p $ 3 *\<^sub>R vector2_append1 (cart2_pt p) = proj2_rep p

goal (1 subgoal):
 1. proj2_pt (cart2_pt p) = p
[PROOF STEP]
with \<open>z_non_zero p\<close>
    and proj2_abs_mult [of "(proj2_rep p)$3" "vector2_append1 (cart2_pt p)"]
[PROOF STATE]
proof (chain)
picking this:
z_non_zero p
z_non_zero p \<Longrightarrow> proj2_abs (proj2_rep p $ 3 *\<^sub>R vector2_append1 (cart2_pt p)) = proj2_abs (vector2_append1 (cart2_pt p))
proj2_rep p $ 3 *\<^sub>R vector2_append1 (cart2_pt p) = proj2_rep p
[PROOF STEP]
have "proj2_abs (vector2_append1 (cart2_pt p)) = proj2_abs (proj2_rep p)"
[PROOF STATE]
proof (prove)
using this:
z_non_zero p
z_non_zero p \<Longrightarrow> proj2_abs (proj2_rep p $ 3 *\<^sub>R vector2_append1 (cart2_pt p)) = proj2_abs (vector2_append1 (cart2_pt p))
proj2_rep p $ 3 *\<^sub>R vector2_append1 (cart2_pt p) = proj2_rep p

goal (1 subgoal):
 1. proj2_abs (vector2_append1 (cart2_pt p)) = proj2_abs (proj2_rep p)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
proj2_abs (vector2_append1 (cart2_pt p)) = proj2_abs (proj2_rep p)

goal (1 subgoal):
 1. proj2_pt (cart2_pt p) = p
[PROOF STEP]
thus "proj2_pt (cart2_pt p) = p"
[PROOF STATE]
proof (prove)
using this:
proj2_abs (vector2_append1 (cart2_pt p)) = proj2_abs (proj2_rep p)

goal (1 subgoal):
 1. proj2_pt (cart2_pt p) = p
[PROOF STEP]
by (unfold proj2_pt_def) (simp add: proj2_abs_rep)
[PROOF STATE]
proof (state)
this:
proj2_pt (cart2_pt p) = p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cart2_injective:
  assumes "z_non_zero p" and "z_non_zero q" and "cart2_pt p = cart2_pt q"
  shows "p = q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p = q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p = q
[PROOF STEP]
from \<open>z_non_zero p\<close> and \<open>z_non_zero q\<close>
[PROOF STATE]
proof (chain)
picking this:
z_non_zero p
z_non_zero q
[PROOF STEP]
have "proj2_pt (cart2_pt p) = p" and "proj2_pt (cart2_pt q) = q"
[PROOF STATE]
proof (prove)
using this:
z_non_zero p
z_non_zero q

goal (1 subgoal):
 1. proj2_pt (cart2_pt p) = p &&& proj2_pt (cart2_pt q) = q
[PROOF STEP]
by (simp_all add: proj2_cart2)
[PROOF STATE]
proof (state)
this:
proj2_pt (cart2_pt p) = p
proj2_pt (cart2_pt q) = q

goal (1 subgoal):
 1. p = q
[PROOF STEP]
from \<open>proj2_pt (cart2_pt p) = p\<close> and \<open>cart2_pt p = cart2_pt q\<close>
[PROOF STATE]
proof (chain)
picking this:
proj2_pt (cart2_pt p) = p
cart2_pt p = cart2_pt q
[PROOF STEP]
have "proj2_pt (cart2_pt q) = p"
[PROOF STATE]
proof (prove)
using this:
proj2_pt (cart2_pt p) = p
cart2_pt p = cart2_pt q

goal (1 subgoal):
 1. proj2_pt (cart2_pt q) = p
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
proj2_pt (cart2_pt q) = p

goal (1 subgoal):
 1. p = q
[PROOF STEP]
with \<open>proj2_pt (cart2_pt q) = q\<close>
[PROOF STATE]
proof (chain)
picking this:
proj2_pt (cart2_pt q) = q
proj2_pt (cart2_pt q) = p
[PROOF STEP]
show "p = q"
[PROOF STATE]
proof (prove)
using this:
proj2_pt (cart2_pt q) = q
proj2_pt (cart2_pt q) = p

goal (1 subgoal):
 1. p = q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
p = q

goal:
No subgoals!
[PROOF STEP]
qed