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