English
For p1,p2 ∈ P and g ∈ G, p1 -ᵥ (g +ᵥ p2) = p1 -ᵥ p2 - g.
Русский
Для p1,p2 ∈ P и g ∈ G: p1 -ᵥ (g +ᵥ p2) = p1 -ᵥ p2 - g.
LaTeX
$$$p_1 -ᵥ (g +ᵥ p_2) = p_1 -ᵥ p_2 - g$$$
Lean4
/-- Subtracting the result of adding a group element produces the same result
as subtracting the points and subtracting that group element. -/
theorem vsub_vadd_eq_vsub_sub (p₁ p₂ : P) (g : G) : p₁ -ᵥ (g +ᵥ p₂) = p₁ -ᵥ p₂ - g := by
rw [← add_right_inj (p₂ -ᵥ p₁ : G), vsub_add_vsub_cancel, ← neg_vsub_eq_vsub_rev, vadd_vsub, ← add_sub_assoc, ←
neg_vsub_eq_vsub_rev, neg_add_cancel, zero_sub]