English
If x and z lie on the same ray, and y and z lie on the same ray, then x+y also lies on the same ray with z.
Русский
Если x и z лежат на одном луче, а y и z тоже, то x+y лежит на том же луче, что и z.
LaTeX
$$$ \operatorname{SameRay}(R, x, z) \land \operatorname{SameRay}(R, y, z) \Rightarrow \operatorname{SameRay}(R, x+y, z). $$$
Lean4
/-- If `x` and `y` are on the same ray as `z`, then so is `x + y`. -/
theorem add_left (hx : SameRay R x z) (hy : SameRay R y z) : SameRay R (x + y) z :=
by
rcases eq_or_ne x 0 with (rfl | hx₀); · rwa [zero_add]
rcases eq_or_ne y 0 with (rfl | hy₀); · rwa [add_zero]
rcases eq_or_ne z 0 with (rfl | hz₀); · apply zero_right
rcases hx.exists_pos hx₀ hz₀ with ⟨rx, rz₁, hrx, hrz₁, Hx⟩
rcases hy.exists_pos hy₀ hz₀ with ⟨ry, rz₂, hry, hrz₂, Hy⟩
refine Or.inr (Or.inr ⟨rx * ry, ry * rz₁ + rx * rz₂, mul_pos hrx hry, ?_, ?_⟩)
· positivity
· convert congr(ry • $Hx + rx • $Hy) using 1 <;> module
