English
If x, y, z are in a betweenness configuration, then Wbtw is equivalent to x ≠ y and z lies in a certain image with Ioi.
Русский
Если x, y, z удовлетворяют betweenness, то Wbtw эквивалентно x ≠ y и z лежит в области образа с Ioi.
LaTeX
$$Sbtw with Ioi equivalence$$
Lean4
theorem wbtw_iff_of_le {x y z : R} (hxz : x ≤ z) : Wbtw R x y z ↔ x ≤ y ∧ y ≤ z := by
cases hxz.eq_or_lt with
| inl hxz =>
subst hxz
rw [← le_antisymm_iff, wbtw_self_iff, eq_comm]
| inr hxz =>
have hxz' : 0 < z - x := sub_pos.mpr hxz
let r := (y - x) / (z - x)
have hy : y = r * (z - x) + x := by simp [r, hxz'.ne']
simp [hy, wbtw_mul_sub_add_iff, mul_nonneg_iff_of_pos_right hxz', ← le_sub_iff_add_le, mul_le_iff_le_one_left hxz',
hxz.ne]
