proposition: Theorem FulpFPredGePos : forall f : float, Fbounded b f -> Fcanonic radix b f -> (0 < f)%R -> (Fulp (FPred b radix precision f) <= Fulp f)%R.
proof: Proof. intros f Hf1 Hf2 H. apply LeFulpPos; auto with zarith; unfold FtoRradix in |- *. apply FBoundedPred; auto with zarith. apply R0RltRlePred; auto with zarith. apply Rlt_le; apply FPredLt; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz