∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x : V},
  x ≠ 0 →
    ∀ (r : ℝ), o.oangle (r • (o.rotation ↑(Real.pi / 2)) x) (r • (o.rotation ↑(Real.pi / 2)) x - x) = ↑(Real.arctan r⁻¹)