proposition: Theorem RoundedModeRep : forall P, RoundedModeP P -> forall p q : float, P p q -> exists m : Z, q = Float m (Fexp p) :>R.
proof: Proof. intros P H' p q H'0. apply MinOrMaxRep with (P := P); auto with zarith. apply H'. Qed.
imports: Reals ZArith List PeanoNat Psatz