… and bisection lemmas

Add lemmas

```lean
lemma oangle_eq_neg_of_angle_eq_of_sign_eq_neg {w x y z : V}
    (h : InnerProductGeometry.angle w x = InnerProductGeometry.angle y z)
    (hs : (o.oangle w x).sign = -(o.oangle y z).sign) : o.oangle w x = -o.oangle y z := by
```

and

```lean
lemma angle_eq_iff_oangle_eq_neg_of_sign_eq_neg {w x y z : V} (hw : w ≠ 0) (hx : x ≠ 0)
    (hy : y ≠ 0) (hz : z ≠ 0) (hs : (o.oangle w x).sign = -(o.oangle y z).sign) :
    InnerProductGeometry.angle w x = InnerProductGeometry.angle y z ↔
      o.oangle w x = -o.oangle y z := by
```

and similar affine versions, corresponding to such lemmas that already
exist when the signs are equal rather than negations of each other.
Deduce lemmas relating oriented and unoriented versions of angle
bisection:

```lean
lemma angle_eq_iff_oangle_eq_or_sameRay {x y z : V} (hx : x ≠ 0) (hz : z ≠ 0) :
    InnerProductGeometry.angle x y = InnerProductGeometry.angle y z ↔
      o.oangle x y = o.oangle y z ∨ SameRay ℝ x z := by
```

and

```lean
lemma angle_eq_iff_oangle_eq_or_wbtw {p₁ p₂ p₃ p₄ : P} (hp₁ : p₁ ≠ p₂) (hp₄ : p₄ ≠ p₂) :
    ∠ p₁ p₂ p₃ = ∠ p₃ p₂ p₄ ↔ ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄ ∨ Wbtw ℝ p₂ p₁ p₄ ∨ Wbtw ℝ p₂ p₄ p₁ := by
```

… equal distance

Add a lemma

```lean
lemma dist_orthogonalProjection_eq_iff_oangle_eq {p p' : P} {s₁ s₂ : AffineSubspace ℝ P}
    [s₁.direction.HasOrthogonalProjection] [s₂.direction.HasOrthogonalProjection]
    (hp' : p' ∈ s₁ ⊓ s₂)
    (hne : haveI : Nonempty s₁ := ⟨p', hp'.1⟩; haveI : Nonempty s₂ := ⟨p', hp'.2⟩;
      (orthogonalProjection s₁ p : P) ≠ orthogonalProjection s₂ p)
    (hp₁ : haveI : Nonempty s₁ := ⟨p', hp'.1⟩; orthogonalProjection s₁ p ≠ p')
    (hp₂ : haveI : Nonempty s₂ := ⟨p', hp'.2⟩; orthogonalProjection s₂ p ≠ p') :
    haveI : Nonempty s₁ := ⟨p', hp'.1⟩
    haveI : Nonempty s₂ := ⟨p', hp'.2⟩
    dist p (orthogonalProjection s₁ p) = dist p (orthogonalProjection s₂ p) ↔
      ∡ (orthogonalProjection s₁ p : P) p' p = ∡ p p' (orthogonalProjection s₂ p) :=
```

that is an oriented angle analogue of the existing
`dist_orthogonalProjection_eq_iff_angle_eq`.  Because the minimal
nondegeneracy conditions required for the two directions of this lemma
are different (whereas the unoriented version doesn't need any
nondegeneracy conditions), those two directions are added as separate
lemmas, each with minimal nondegeneracy conditions, from which the
`iff` version is then deduced.

…ality of twice angles

Add lemmas that two angles less than `π / 2` are equal if and only if
twice those angles are equal, along with a separate lemma

```lean
lemma toReal_neg_eq_neg_toReal_iff {θ : Angle} : (-θ).toReal = -(θ.toReal) ↔ θ ≠ π := by
```

which isn't directly connected but turns out to be useful in the same
application (dealing with angles in right-angled triangles that are
less then `π / 2`, when you have two such triangles that are
oppositely-oriented).

…`π / 2`

Add a lemma that an oriented angle in a right-angled triangle is less
than `π / 2`, even in degenerate cases (there's already a
corresponding lemma for unoriented angles, but that one needs to
exclude some degenerate cases because of the different default values
for oriented and unoriented angles involving zero vectors).  Deduce
lemmas that, for such angles involved in right-angled triangles,
equality of the angles (i.e. equality mod 2π) follows from equality of
twice the angles (i.e. equality of the angles mod π).

Add a lemma

```lean
lemma orthogonalProjection_eq_iff_mem {s : AffineSubspace ℝ P} [Nonempty s]
    [s.direction.HasOrthogonalProjection] {p q : P} :
    orthogonalProjection s p = q ↔ q ∈ s ∧ p -ᵥ q ∈ s.directionᗮ := by
```

that gives the characteristic property of the orthogonal projection in
a more convenient form to use than the existing
`inter_eq_singleton_orthogonalProjection` (from which it is derived).

…ion_orthogonalProjection_of_le

…isector_dist_oangle

Add instances that the supremum of two affine subspaces, either one
nonempty, is nonempty.  These are useful when working with orthogonal projections onto such a supremum.

…ion_sup_of_orthogonalProjection_eq

Add a lemma that, if the orthogonal projections of a point onto two
subspaces are equal, so is the projection onto their supremum.

Co-authored-by: Eric Wieser <[email protected]>

…sup_of_orthogonalProjection_eq

…ion_orthogonalProjection_of_le

…isector_dist_oangle

…ion_sup_of_orthogonalProjection_eq

…ion_orthogonalProjection_of_le

…isector_dist_oangle

…ion_sup_of_orthogonalProjection_eq

Co-authored-by: Eric Wieser <[email protected]>

…ion_orthogonalProjection_of_le

…isector_dist_oangle