Oriented angle is a right angle if unoriented angle is

Stream: Is there code for X?

[Eric Wieser]

I've seen 2 • a = π used quite often to indicate that an oriented a : Real.angle is a right angle; do we have a way to translate to the unoriented version?

import Mathlib

variable {V : Type*}
variable [NormedAddCommGroup V] [InnerProductSpace ℝ V]
variable [Fact (FiniteDimensional.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)]

open Real

example {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) :
    2 • positiveOrientation.oangle x y = ↑π ↔ 2 • InnerProductGeometry.angle x y = π := by
  sorry

[Eric Wieser]

docs#Orientation.oangle_eq_pi_iff_angle_eq_pi is very close, but missing the factors of two

[Joseph Myers]

We don't seem to have this particular statement, but some combination of eq_zero_or_oangle_eq_iff_inner_eq_zero and inner_eq_zero_iff_angle_eq_pi_div_two and Real.Angle.two_nsmul_eq_pi_iff should be usable to prove it.