[float_unbounded] fix the sqrt and comparison wrappers

[Robertboy18]

hey, this fixes the two wrapper copy/paste issues from #25 and #26.

changes:

• sqt_f32/sqt_d64 now call Ssqrt/Dsqrt instead of abs
• > and >= now flip the operands like the core float.pvs definitions do
• same fix for the float-to-real overloads

checked it with PVS 8.1:

• focused regression checks pass 10/10 for binary32 and binary64
• ./prove-all -do=float/float_unbounded passes all 918/918 proofs

so yeah, just wiring the convenience API back to the operations it was supposed to use!

[Copilot]

Pull request overview

This PR fixes copy/paste mistakes in the float/float_unbounded convenience theories so their wrapper operators/functions match the intended underlying IEEE-754 operations and operand order.

Changes:

• Fix sqt_f32 / sqt_d64 to call Ssqrt / Dsqrt (instead of Sabs / Dabs).
• Fix > and >= wrappers (and the real overloads) to flip operands, matching the core float.pvs operator definitions.
• Add/update the generated proveit proof summary for float/float_unbounded.

Reviewed changes

Copilot reviewed 3 out of 3 changed files in this pull request and generated no comments.

File	Description
summaries/float-float_unbounded.summary	Adds updated proveit run summary showing all float/float_unbounded proofs succeeding.
float/float_unbounded/float32.pvs	Corrects sqt_f32 wrapper to use Ssqrt and fixes >/>= operand order (including (x, real) overloads).
float/float_unbounded/double64.pvs	Corrects sqt_d64 wrapper to use Dsqrt and fixes >/>= operand order (including (x, real) overloads).

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.