Real correctness of rational-power comparisons

The exact equality test is complete for positive bases, and the logarithm enclosures contain the exact difference. Since the logarithm is strictly increasing on positive values, the sign of that difference is the ordering of the power and the target. Zero bases, unit bases and zero exponents are covered by direct evaluation.

theorem FloatLib.Numerics.RationalPower.compare_eq_real (base exponent target : ℚ) (hbase : 0 ≤ base) : compare base exponent target = cmp (↑base ^ ↑exponent) ↑target

For every base ≥ 0, compare returns the ordering of the real power and the target.