English
If Wbtw w y z and Wbtw w x y, then Wbtw x y z.
Русский
Если Wbtw w y z и Wbtw w x y, тогда Wbtw x y z.
LaTeX
$$$(Wbtw_R w y z) \land (Wbtw_R w x y) \Rightarrow Wbtw_R x y z$$$
Lean4
theorem trans_left_right {w x y z : P} (h₁ : Wbtw R w y z) (h₂ : Wbtw R w x y) : Wbtw R x y z :=
by
rcases h₁ with ⟨t₁, ht₁, rfl⟩
rcases h₂ with ⟨t₂, ht₂, rfl⟩
refine
⟨(t₁ - t₂ * t₁) / (1 - t₂ * t₁),
⟨div_nonneg (sub_nonneg.2 (mul_le_of_le_one_left ht₁.1 ht₂.2)) (sub_nonneg.2 (mul_le_one₀ ht₂.2 ht₁.1 ht₁.2)),
div_le_one_of_le₀ (sub_le_sub_right ht₁.2 _) (sub_nonneg.2 (mul_le_one₀ ht₂.2 ht₁.1 ht₁.2))⟩,
?_⟩
simp only [lineMap_apply, smul_smul, ← add_vadd, vsub_vadd_eq_vsub_sub, smul_sub, ← sub_smul, ← add_smul, vadd_vsub,
vadd_right_cancel_iff, div_mul_eq_mul_div, div_sub_div_same]
nth_rw 1 [← mul_one (t₁ - t₂ * t₁)]
rw [← mul_sub, mul_div_assoc]
by_cases h : 1 - t₂ * t₁ = 0
· rw [sub_eq_zero, eq_comm] at h
rw [h]
suffices t₁ = 1 by simp [this]
exact eq_of_le_of_not_lt ht₁.2 fun ht₁lt => (mul_lt_one_of_nonneg_of_lt_one_right ht₂.2 ht₁.1 ht₁lt).ne h
· rw [div_self h]
ring_nf
