mathlib3

f1f9d66a - feat(analysis/convex/between): `wbtw` and distinct end points (#16768)

feat(analysis/convex/between): `wbtw` and distinct end points (#16768) Add lemmas that `wbtw`, together with the middle point being distinct from one of the end points, implies the two end points are distinct, and use one of those lemmas in the proof of `sbtw.left_ne_right`.