[STATEMENT]
lemma cosh_dist_perp_divide:
  assumes "M_perp l m" and "a \<in> hyp2" and "b \<in> hyp2" and "c \<in> hyp2"
  and "proj2_incident a l" and "proj2_incident b l" and "proj2_incident b m"
  and "proj2_incident c m"
  shows "cosh_dist b c = cosh_dist a c / cosh_dist b a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cosh_dist b c = cosh_dist a c / cosh_dist b a
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cosh_dist b c = cosh_dist a c / cosh_dist b a
[PROOF STEP]
from \<open>b \<in> hyp2\<close> and \<open>a \<in> hyp2\<close>
[PROOF STATE]
proof (chain)
picking this:
b \<in> hyp2
a \<in> hyp2
[PROOF STEP]
have "cosh_dist b a > 0"
[PROOF STATE]
proof (prove)
using this:
b \<in> hyp2
a \<in> hyp2

goal (1 subgoal):
 1. 0 < cosh_dist b a
[PROOF STEP]
by (rule cosh_dist_positive)
[PROOF STATE]
proof (state)
this:
0 < cosh_dist b a

goal (1 subgoal):
 1. cosh_dist b c = cosh_dist a c / cosh_dist b a
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
M_perp l m
a \<in> hyp2
b \<in> hyp2
c \<in> hyp2
proj2_incident a l
proj2_incident b l
proj2_incident b m
proj2_incident c m
[PROOF STEP]
have "cosh_dist a c = cosh_dist b a * cosh_dist b c"
[PROOF STATE]
proof (prove)
using this:
M_perp l m
a \<in> hyp2
b \<in> hyp2
c \<in> hyp2
proj2_incident a l
proj2_incident b l
proj2_incident b m
proj2_incident c m

goal (1 subgoal):
 1. cosh_dist a c = cosh_dist b a * cosh_dist b c
[PROOF STEP]
by (rule cosh_dist_perp)
[PROOF STATE]
proof (state)
this:
cosh_dist a c = cosh_dist b a * cosh_dist b c

goal (1 subgoal):
 1. cosh_dist b c = cosh_dist a c / cosh_dist b a
[PROOF STEP]
with \<open>cosh_dist b a > 0\<close>
[PROOF STATE]
proof (chain)
picking this:
0 < cosh_dist b a
cosh_dist a c = cosh_dist b a * cosh_dist b c
[PROOF STEP]
show "cosh_dist b c = cosh_dist a c / cosh_dist b a"
[PROOF STATE]
proof (prove)
using this:
0 < cosh_dist b a
cosh_dist a c = cosh_dist b a * cosh_dist b c

goal (1 subgoal):
 1. cosh_dist b c = cosh_dist a c / cosh_dist b a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cosh_dist b c = cosh_dist a c / cosh_dist b a

goal:
No subgoals!
[PROOF STEP]
qed