Another Sbtw transitivity theorem?

Stream: Is there code for X?

[Chu Zheng]

Hi, I couldn't find the following theorem in the library; do we already have it?

import Mathlib.LinearAlgebra.AffineSpace.Independent
import Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
import Mathlib.Geometry.Euclidean.Simplex

open Module Affine Simplex EuclideanGeometry Real

variable {V : Type*} {Pt : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace Pt]
  [NormedAddTorsor V Pt]

theorem Sbtw.extend {a b c d : Pt}
    (h₁ : Sbtw ℝ a b c) (h₂ : Sbtw ℝ b c d) :
    Sbtw ℝ a b d := by
  sorry

It seems like the existing lemmas named Sbtw.trans_left Sbtw.trans_right Sbtw.trans_left_right Sbtw.trans_right_left(Mathlib.Analysis.Convex.Between). but none seemed to match this shape.

I tried to prove this using lineMap but got stuck on the final simplification step.

[Yury G. Kudryashov]

Some Sbtw transitivity theorems are definitely missing. Here is the complete list of lemmas with conclusion Sbtw _ _ _ _: @loogle |- Sbtw ..

[loogle]

:search: Sbtw.symm, Sbtw.const_vsub, and 24 more

[Yury G. Kudryashov]

A PR with the missing lemmas would be very welcome!