English
If the oriented angle sign equals one, then the oriented angle equals the unoriented angle (as a real angle).
Русский
Если знак ориентированного угла равен единице, то сам ориентированный угол равен неориентированному углу (как вещественный угол).
LaTeX
$$$ (o.oangle x y).sign = 1 \Rightarrow o.oangle x y = Real.Angle.coe (InnerProductGeometry.angle x y) $$$
Lean4
/-- The oriented angle between two vectors equals the unoriented angle if the sign is positive. -/
theorem oangle_eq_angle_of_sign_eq_one {x y : V} (h : (o.oangle x y).sign = 1) :
o.oangle x y = InnerProductGeometry.angle x y :=
by
by_cases hx : x = 0; · simp [hx] at h
by_cases hy : y = 0; · simp [hy] at h
refine (o.oangle_eq_angle_or_eq_neg_angle hx hy).resolve_right ?_
intro hxy
rw [hxy, Real.Angle.sign_neg, neg_eq_iff_eq_neg, ← SignType.neg_iff, ← not_le] at h
exact
h
(Real.Angle.sign_coe_nonneg_of_nonneg_of_le_pi (InnerProductGeometry.angle_nonneg _ _)
(InnerProductGeometry.angle_le_pi _ _))
