feat(algebra/add_torsor): more cancellation lemmas (#3368)

Add more cancellation lemmas for `vsub`, similar to lemmas already
present for `vadd`.

Author: jsm28

src/algebra/add_torsor.lean

@@ -244,6 +244,32 @@ end
   ((v₁ +ᵥ p) -ᵥ (v₂ +ᵥ p) : G) = v₁ - v₂ :=
 by rw [vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, vsub_self, add_zero]
 
+/-- If the same point subtracted from two points produces equal
+results, those points are equal. -/
+lemma vsub_left_cancel {p1 p2 p : P} (h : (p1 -ᵥ p : G) = p2 -ᵥ p) : p1 = p2 :=
+by rwa [←sub_eq_zero, vsub_sub_vsub_cancel_right, vsub_eq_zero_iff_eq] at h
+
+/-- The same point subtracted from two points produces equal results
+if and only if those points are equal. -/
+@[simp] lemma vsub_left_cancel_iff {p1 p2 p : P} : (p1 -ᵥ p : G) = p2 -ᵥ p ↔ p1 = p2 :=
+⟨vsub_left_cancel _, λ h, h ▸ rfl⟩
+
+/-- If subtracting two points from the same point produces equal
+results, those points are equal. -/
+lemma vsub_right_cancel {p1 p2 p : P} (h : (p -ᵥ p1 : G) = p -ᵥ p2) : p1 = p2 :=
+begin
+  have h2 : (p -ᵥ p2 : G) +ᵥ p1 = (p -ᵥ p1 : G) +ᵥ p1, { rw h },
+  conv_rhs at h2 {
+    rw [vsub_vadd, ←vsub_vadd G p p2],
+  },
+  rwa vadd_left_cancel_iff at h2
+end
+
+/-- Subtracting two points from the same point produces equal results
+if and only if those points are equal. -/
+@[simp] lemma vsub_right_cancel_iff {p1 p2 p : P} : (p -ᵥ p1 : G) = p -ᵥ p2 ↔ p1 = p2 :=
+⟨vsub_right_cancel _, λ h, h ▸ rfl⟩
+
 end general
 
 section comm