Theorem: length_lt_of_length_lt
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.inl.intro.intro.intro.refine'_2
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
abc_def : angle a b c = angle d e f
lineq : length d f < length a c
df : d ≠ f
ac : a ≠ c
ab : a ≠ b
bc : b ≠ c
AC : line
aAC : online a AC
cAC : online c AC
AB : line
aAB : online a AB
bAB : online b AB
BC : line
bBC : online b BC
cBC : online c BC
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
gAC : online g AC
gBC : ¬online g BC
gAB : ¬online g AB
contra : length a b < length d e
h : point
bac_edf : angle h a g = angle e d f
Hh : B a b h ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
hAB : online h AB
hg : h ≠ g
hAC : ¬online h AC
hag_bac : angle h a g = angle b a c
ang : length g h = length f e ∧ angle a g h = angle d f e ∧ angle a h g = angle a b c
this : para HG BC
ss1 : sameside h g BC
⊢ False

case intro.intro.intro.intro.intro.intro.intro.inl.intro.intro.intro.refine'_1
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
abc_def : angle a b c = angle d e f
lineq : length d f < length a c
df : d ≠ f
ac : a ≠ c
ab : a ≠ b
bc : b ≠ c
AC : line
aAC : online a AC
cAC : online c AC
AB : line
aAB : online a AB
bAB : online b AB
BC : line
bBC : online b BC
cBC : online c BC
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
gAC : online g AC
gBC : ¬online g BC
gAB : ¬online g AB
contra : length a b < length d e
h : point
bac_edf : angle h a g = angle e d f
Hh : B a b h ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
hAB : online h AB
hg : h ≠ g
hAC : ¬online h AC
hag_bac : angle h a g = angle b a c
ang : length g h = length f e ∧ angle a g h = angle d f e ∧ angle a h g = angle a b c
⊢ sameside c g AB
Tactic:
have ss2 := sameside_of_B_not_online_2 (B_symm Hg.1) cBC gBC
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.inl.intro.intro.intro.refine'_2
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
abc_def : angle a b c = angle d e f
lineq : length d f < length a c
df : d ≠ f
ac : a ≠ c
ab : a ≠ b
bc : b ≠ c
AC : line
aAC : online a AC
cAC : online c AC
AB : line
aAB : online a AB
bAB : online b AB
BC : line
bBC : online b BC
cBC : online c BC
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
gAC : online g AC
gBC : ¬online g BC
gAB : ¬online g AB
contra : length a b < length d e
h : point
bac_edf : angle h a g = angle e d f
Hh : B a b h ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
hAB : online h AB
hg : h ≠ g
hAC : ¬online h AC
hag_bac : angle h a g = angle b a c
ang : length g h = length f e ∧ angle a g h = angle d f e ∧ angle a h g = angle a b c
this : para HG BC
ss1 : sameside h g BC
ss2 : sameside g a BC
⊢ False

case intro.intro.intro.intro.intro.intro.intro.inl.intro.intro.intro.refine'_1
i : incidence_geometry
a b c d e f : point
Tabc : ¬colinear a b c
Tdef : ¬colinear d e f
abc_def : angle a b c = angle d e f
lineq : length d f < length a c
df : d ≠ f
ac : a ≠ c
ab : a ≠ b
bc : b ≠ c
AC : line
aAC : online a AC
cAC : online c AC
AB : line
aAB : online a AB
bAB : online b AB
BC : line
bBC : online b BC
cBC : online c BC
bAC : ¬online b AC
g : point
Hg : B a g c ∧ length a g = length d f
gAC : online g AC
gBC : ¬online g BC
gAB : ¬online g AB
contra : length a b < length d e
h : point
bac_edf : angle h a g = angle e d f
Hh : B a b h ∧ length a h = length d e
HG : line
hHG : online h HG
gHG : online g HG
hAB : online h AB
hg : h ≠ g
hAC : ¬online h AC
hag_bac : angle h a g = angle b a c
ang : length g h = length f e ∧ angle a g h = angle d f e ∧ angle a h g = angle a b c
⊢ sameside c g AB