proposition: Theorem FPredLt : forall a : float, (FPred a < a)%R.
proof: Proof. intros a; rewrite FPredFopFSucc. pattern a at 2 in |- *; rewrite <- (Fopp_Fopp a). unfold FtoRradix in |- *; repeat rewrite Fopp_correct. apply Ropp_lt_contravar. rewrite <- Fopp_correct; auto with zarith. apply FSuccLt; try easy. Qed.
imports: Reals ZArith List PeanoNat Psatz