English
If x and y lie on the same ray, then the norm of their difference equals the absolute value of the difference of their norms.
Русский
Если x и y лежат на одном луче, то норма разности равна модулю разности норм.
LaTeX
$$$$ \text{If } \text{SameRay}(\mathbb{R},x,y) \text{ then } \|x-y\| = |\|x\| - \|y\||. $$$$
Lean4
theorem norm_sub (h : SameRay ℝ x y) : ‖x - y‖ = |‖x‖ - ‖y‖| :=
by
rcases h.exists_eq_smul with ⟨u, a, b, ha, hb, -, rfl, rfl⟩
wlog hab : b ≤ a generalizing a b with H
· rw [SameRay.sameRay_comm] at h
rw [norm_sub_rev, abs_sub_comm]
exact H b a hb ha h (le_of_not_ge hab)
rw [← sub_nonneg] at hab
rw [← sub_smul, norm_smul_of_nonneg hab, norm_smul_of_nonneg ha, norm_smul_of_nonneg hb, ← sub_mul,
abs_of_nonneg (mul_nonneg hab (norm_nonneg _))]
