Correctly rounded two-coordinate posit arctangent

The Posit Standard (2022), §5.5, orders the coordinates as (x, y): the result is the principal argument of x + i*y. The negative real axis has angle pi. NaR propagates, and the origin produces NaR rather than adopting Mathlib's totalized zero angle.

The pi-scaled variant divides the exact angle by pi before the final rounding.

def FloatLib.Floats.Formats.Posit.Model.Trigonometric.evaluateArgument {format : Format} (prepare : ℚ → ℚ → ℕ → Numerics.Enclosure.Comparison.Prepared) (x y : Model format) : Model format

Decode both coordinates, reject the origin, and round using the supplied comparator. Its exact argument semantics are the hypothesis of evaluateArgument_eq_real.

def FloatLib.Floats.Formats.Posit.Model.arcTan2 {format : Format} (x y : Model format) : Model format

Correctly rounded principal argument of x + i*y, in radians; (0, 0) produces NaR.

def FloatLib.Floats.Formats.Posit.Model.arcTan2Pi {format : Format} (x y : Model format) : Model format

Correctly rounded principal argument of x + i*y divided by pi; (0, 0) produces NaR.