feat(geometry/euclidean/angle/oriented/affine): more collinearity / a…

…ffine independence lemmas (#17815)

Add lemmas that, if twice the oriented angles between two triples of points are equal, one triple is affinely independent / collinear if and only if the other triple is.

src/geometry/euclidean/angle/oriented/affine.lean

@@ -200,6 +200,20 @@ lemma oangle_eq_zero_or_eq_pi_iff_collinear {p₁ p₂ p₃ : P} :
 by rw [←not_iff_not, not_or_distrib, oangle_ne_zero_and_ne_pi_iff_affine_independent,
        affine_independent_iff_not_collinear_set]
 
+/-- If twice the oriented angles between two triples of points are equal, one triple is affinely
+independent if and only if the other is. -/
+lemma affine_independent_iff_of_two_zsmul_oangle_eq {p₁ p₂ p₃ p₄ p₅ p₆ : P}
+  (h : (2 : ℤ) • ∡ p₁ p₂ p₃ = (2 : ℤ) • ∡ p₄ p₅ p₆) :
+  affine_independent ℝ ![p₁, p₂, p₃] ↔ affine_independent ℝ ![p₄, p₅, p₆] :=
+by simp_rw [←oangle_ne_zero_and_ne_pi_iff_affine_independent, ←real.angle.two_zsmul_ne_zero_iff, h]
+
+/-- If twice the oriented angles between two triples of points are equal, one triple is collinear
+if and only if the other is. -/
+lemma collinear_iff_of_two_zsmul_oangle_eq {p₁ p₂ p₃ p₄ p₅ p₆ : P}
+  (h : (2 : ℤ) • ∡ p₁ p₂ p₃ = (2 : ℤ) • ∡ p₄ p₅ p₆) :
+  collinear ℝ ({p₁, p₂, p₃} : set P) ↔ collinear ℝ ({p₄, p₅, p₆} : set P) :=
+by simp_rw [←oangle_eq_zero_or_eq_pi_iff_collinear, ←real.angle.two_zsmul_eq_zero_iff, h]
+
 /-- Given three points not equal to `p`, the angle between the first and the second at `p` plus
 the angle between the second and the third equals the angle between the first and the third. -/
 @[simp] lemma oangle_add {p p₁ p₂ p₃ : P} (hp₁ : p₁ ≠ p) (hp₂ : p₂ ≠ p) (hp₃ : p₃ ≠ p) :