feat(analysis/special_functions/trigonometric/angle): equality of `cos` or `sin` (#15651)
`analysis.special_functions.trigonometric.angle` has results relating
equality of `real.cos` of two reals, or `real.sin` of two reals, to
relations between those reals converted to `angle`. Add variants of
those results where one or both of the arguments are passed as `angle`
instead of as reals, with `real.angle.cos` and `real.angle.sin` used
on those `angle` arguments.
The version for `cos` with one `angle` and one real argument, in
particular, is what I want for proving that the oriented angle between
two nonzero vectors is plus or minus the unoriented angle.
mathlib
63eb48be - feat(analysis/special_functions/trigonometric/angle): equality of `cos` or `sin` (#15651)
