proposition: Theorem FNPredLt : forall a : float, (FNPred a < a)%R.
proof: Proof. intros a; unfold FNPred in |- *. unfold FtoRradix in |- *; rewrite <- (FnormalizeCorrect _ radixMoreThanOne b precision a). apply FPredLt; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz