proposition: Theorem MinOrMaxRep : forall P, MinOrMaxP 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; case (H' p q); auto; intros H'1. apply FminRep with (3 := pGivesBound); auto with zarith. apply FmaxRep with (3 := pGivesBound); auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz