Coercion lemmas for ℝ → EReal

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

This file centralizes small “coe distributes over min/max” rewrite lemmas for the interval soundness modules.

We do not mark these as simp lemmas: they are intended for targeted rewriting in interval proofs, and we want to avoid surprising simp behavior in unrelated developments.

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

Coercion distributes over min for reals embedded into EReal.

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

Coercion distributes over max for reals embedded into EReal.