proposition: Theorem FulpPred : forall p : float, Fbounded b p -> (p - FNPred b radix precision p <= Fulp p)%R.
proof: Proof. intros p H'. replace (Fulp p) with (Fulp (Fnormalize radix b precision p)). replace (FtoRradix p) with (FtoRradix (Fnormalize radix b precision p)). unfold FNPred in |- *; apply FulpPredCan; auto with arith. apply FnormalizeCanonic; auto with zarith. unfold FtoRradix in |- *; apply FnormalizeCorrect; auto. apply FulpComp; auto with zarith. apply FnormalizeBounded; auto with zarith. unfold FtoRradix in |- *; apply FnormalizeCorrect; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz