exact eqn_8 habc hacd
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z a b c d : V
P : List V
habc : SimpleTriangle a b c
hacd : sbtw a c d
hbd' : b ≠ d
hbd : ¬SimpleEdges.Adj b d
hP' : ∀ (P' : List V), List.Special a b d P' → P.pathLength ≤ P'.pathLength
⊢ dist a b + dist b d < dist a d + Delta a b c
no goals