[STATEMENT]
lemma cross_ratio_not_zero:
  assumes "z \<noteq> u" and "v \<noteq> w"
  shows "cross_ratio z u v w \<noteq> 0\<^sub>h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cross_ratio z u v w \<noteq> 0\<^sub>h
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
z \<noteq> u
v \<noteq> w

goal (1 subgoal):
 1. cross_ratio z u v w \<noteq> 0\<^sub>h
[PROOF STEP]
proof (transfer, transfer)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>z u v w za ua va wa. \<lbrakk>z \<noteq> vec_zero; u \<noteq> vec_zero; v \<noteq> vec_zero; w \<noteq> vec_zero; \<not> z \<approx>\<^sub>v u; \<not> v \<approx>\<^sub>v w; \<not> za \<approx> ua; \<not> va \<approx> wa\<rbrakk> \<Longrightarrow> \<not> cross_ratio_cvec z u v w \<approx>\<^sub>v 0\<^sub>v
[PROOF STEP]
fix z u v w
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>z u v w za ua va wa. \<lbrakk>z \<noteq> vec_zero; u \<noteq> vec_zero; v \<noteq> vec_zero; w \<noteq> vec_zero; \<not> z \<approx>\<^sub>v u; \<not> v \<approx>\<^sub>v w; \<not> za \<approx> ua; \<not> va \<approx> wa\<rbrakk> \<Longrightarrow> \<not> cross_ratio_cvec z u v w \<approx>\<^sub>v 0\<^sub>v
[PROOF STEP]
assume nz: "z \<noteq> vec_zero" "u \<noteq> vec_zero" "v \<noteq> vec_zero" "w \<noteq> vec_zero"
[PROOF STATE]
proof (state)
this:
z \<noteq> vec_zero
u \<noteq> vec_zero
v \<noteq> vec_zero
w \<noteq> vec_zero

goal (1 subgoal):
 1. \<And>z u v w za ua va wa. \<lbrakk>z \<noteq> vec_zero; u \<noteq> vec_zero; v \<noteq> vec_zero; w \<noteq> vec_zero; \<not> z \<approx>\<^sub>v u; \<not> v \<approx>\<^sub>v w; \<not> za \<approx> ua; \<not> va \<approx> wa\<rbrakk> \<Longrightarrow> \<not> cross_ratio_cvec z u v w \<approx>\<^sub>v 0\<^sub>v
[PROOF STEP]
obtain z1 z2 u1 u2 v1 v2 w1 w2 where *: "z = (z1, z2)" "u = (u1, u2)" "v = (v1, v2)" "w = (w1, w2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>z1 z2 u1 u2 v1 v2 w1 w2. \<lbrakk>z = (z1, z2); u = (u1, u2); v = (v1, v2); w = (w1, w2)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases z, cases u, cases v, cases w, auto)
[PROOF STATE]
proof (state)
this:
z = (z1, z2)
u = (u1, u2)
v = (v1, v2)
w = (w1, w2)

goal (1 subgoal):
 1. \<And>z u v w za ua va wa. \<lbrakk>z \<noteq> vec_zero; u \<noteq> vec_zero; v \<noteq> vec_zero; w \<noteq> vec_zero; \<not> z \<approx>\<^sub>v u; \<not> v \<approx>\<^sub>v w; \<not> za \<approx> ua; \<not> va \<approx> wa\<rbrakk> \<Longrightarrow> \<not> cross_ratio_cvec z u v w \<approx>\<^sub>v 0\<^sub>v
[PROOF STEP]
obtain x1 x2 where **: "cross_ratio_cvec z u v w = (x1, x2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x1 x2. cross_ratio_cvec z u v w = (x1, x2) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases "cross_ratio_cvec z u v w", auto)
[PROOF STATE]
proof (state)
this:
cross_ratio_cvec z u v w = (x1, x2)

goal (1 subgoal):
 1. \<And>z u v w za ua va wa. \<lbrakk>z \<noteq> vec_zero; u \<noteq> vec_zero; v \<noteq> vec_zero; w \<noteq> vec_zero; \<not> z \<approx>\<^sub>v u; \<not> v \<approx>\<^sub>v w; \<not> za \<approx> ua; \<not> va \<approx> wa\<rbrakk> \<Longrightarrow> \<not> cross_ratio_cvec z u v w \<approx>\<^sub>v 0\<^sub>v
[PROOF STEP]
assume "\<not> z \<approx>\<^sub>v u" "\<not> v \<approx>\<^sub>v w"
[PROOF STATE]
proof (state)
this:
\<not> z \<approx>\<^sub>v u
\<not> v \<approx>\<^sub>v w

goal (1 subgoal):
 1. \<And>z u v w za ua va wa. \<lbrakk>z \<noteq> vec_zero; u \<noteq> vec_zero; v \<noteq> vec_zero; w \<noteq> vec_zero; \<not> z \<approx>\<^sub>v u; \<not> v \<approx>\<^sub>v w; \<not> za \<approx> ua; \<not> va \<approx> wa\<rbrakk> \<Longrightarrow> \<not> cross_ratio_cvec z u v w \<approx>\<^sub>v 0\<^sub>v
[PROOF STEP]
hence "z1*u2 \<noteq> z2*u1" "v1*w2 \<noteq> v2*w1"
[PROOF STATE]
proof (prove)
using this:
\<not> z \<approx>\<^sub>v u
\<not> v \<approx>\<^sub>v w

goal (1 subgoal):
 1. z1 * u2 \<noteq> z2 * u1 &&& v1 * w2 \<noteq> v2 * w1
[PROOF STEP]
using * nz complex_cvec_eq_mix
[PROOF STATE]
proof (prove)
using this:
\<not> z \<approx>\<^sub>v u
\<not> v \<approx>\<^sub>v w
z = (z1, z2)
u = (u1, u2)
v = (v1, v2)
w = (w1, w2)
z \<noteq> vec_zero
u \<noteq> vec_zero
v \<noteq> vec_zero
w \<noteq> vec_zero
\<lbrakk>(?z1.0, ?z2.0) \<noteq> vec_zero; (?w1.0, ?w2.0) \<noteq> vec_zero\<rbrakk> \<Longrightarrow> ((?z1.0, ?z2.0) \<approx>\<^sub>v (?w1.0, ?w2.0)) = (?z1.0 * ?w2.0 = ?z2.0 * ?w1.0)

goal (1 subgoal):
 1. z1 * u2 \<noteq> z2 * u1 &&& v1 * w2 \<noteq> v2 * w1
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
z1 * u2 \<noteq> z2 * u1
v1 * w2 \<noteq> v2 * w1

goal (1 subgoal):
 1. \<And>z u v w za ua va wa. \<lbrakk>z \<noteq> vec_zero; u \<noteq> vec_zero; v \<noteq> vec_zero; w \<noteq> vec_zero; \<not> z \<approx>\<^sub>v u; \<not> v \<approx>\<^sub>v w; \<not> za \<approx> ua; \<not> va \<approx> wa\<rbrakk> \<Longrightarrow> \<not> cross_ratio_cvec z u v w \<approx>\<^sub>v 0\<^sub>v
[PROOF STEP]
hence "x1 \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
z1 * u2 \<noteq> z2 * u1
v1 * w2 \<noteq> v2 * w1

goal (1 subgoal):
 1. x1 \<noteq> 0
[PROOF STEP]
using * **
[PROOF STATE]
proof (prove)
using this:
z1 * u2 \<noteq> z2 * u1
v1 * w2 \<noteq> v2 * w1
z = (z1, z2)
u = (u1, u2)
v = (v1, v2)
w = (w1, w2)
cross_ratio_cvec z u v w = (x1, x2)

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

goal (1 subgoal):
 1. \<And>z u v w za ua va wa. \<lbrakk>z \<noteq> vec_zero; u \<noteq> vec_zero; v \<noteq> vec_zero; w \<noteq> vec_zero; \<not> z \<approx>\<^sub>v u; \<not> v \<approx>\<^sub>v w; \<not> za \<approx> ua; \<not> va \<approx> wa\<rbrakk> \<Longrightarrow> \<not> cross_ratio_cvec z u v w \<approx>\<^sub>v 0\<^sub>v
[PROOF STEP]
thus "\<not> cross_ratio_cvec z u v w \<approx>\<^sub>v 0\<^sub>v"
[PROOF STATE]
proof (prove)
using this:
x1 \<noteq> 0

goal (1 subgoal):
 1. \<not> cross_ratio_cvec z u v w \<approx>\<^sub>v 0\<^sub>v
[PROOF STEP]
using zero_cvec_z1_zero_iff * **
[PROOF STATE]
proof (prove)
using this:
x1 \<noteq> 0
(?z1.0, ?z2.0) \<noteq> vec_zero \<Longrightarrow> ((?z1.0, ?z2.0) \<approx>\<^sub>v 0\<^sub>v) = (?z1.0 = 0)
z = (z1, z2)
u = (u1, u2)
v = (v1, v2)
w = (w1, w2)
cross_ratio_cvec z u v w = (x1, x2)

goal (1 subgoal):
 1. \<not> cross_ratio_cvec z u v w \<approx>\<^sub>v 0\<^sub>v
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> cross_ratio_cvec z u v w \<approx>\<^sub>v 0\<^sub>v

goal:
No subgoals!
[PROOF STEP]
qed