Coercion lemmas for ℝ → EReal

Several executable interval soundness proofs move between real bounds (proved in ℝ) and overflow-safe endpoint reasoning (done in EReal).

The order-preserving embedding commutes with min and max.

These lemmas are used for explicit rewriting, so importing this module does not change the default simplification of coerced bounds.

theorem FloatLib.Floats.Interval.coe_min (a b : ℝ) : ↑(min a b) = min ↑a ↑b

Coercion distributes over min for reals embedded into EReal.

theorem FloatLib.Floats.Interval.coe_max (a b : ℝ) : ↑(max a b) = max ↑a ↑b

Coercion distributes over max for reals embedded into EReal.