proposition: Theorem R0RltRlePred : forall x : float, (0 < x)%R -> (0 <= FPred x)%R.
proof: Proof. intros x H'; rewrite FPredFopFSucc. unfold FtoRradix in |- *; repeat rewrite Fopp_correct. replace 0%R with (-0)%R; auto with real. apply Ropp_le_contravar. apply R0RltRleSucc; auto. unfold FtoRradix in |- *; repeat rewrite Fopp_correct. replace 0%R with (-0)%R; auto with real. Qed.
imports: Reals ZArith List PeanoNat Psatz