proposition: Theorem MaxFloat : forall x : float, Fbounded b x -> (Rabs x < Float (Zpos (vNum b)) (Fexp x))%R.
proof: Proof. intros. replace (Rabs x) with (FtoR radix (Fabs x)). unfold FtoRradix in |- *. apply maxMax with (b := b); auto with *. unfold FtoRradix in |- *. apply Fabs_correct; auto with *. Qed.
imports: Reals ZArith List PeanoNat Psatz