proposition: Theorem boundRCorrect2 : forall r : R, (Fopp (boundR r) < r)%R.
proof: Proof. intros r; case (Rle_or_lt r 0); intros H'. rewrite boundRrOpp. pattern r at 2 in |- *; rewrite <- (Ropp_involutive r). unfold FtoRradix in |- *; rewrite Fopp_correct. apply Ropp_lt_contravar; apply boundRCorrect1; auto. apply Rle_lt_trans with 0%R; auto. replace 0%R with (-0)%R; auto with real. unfold FtoRradix in |- *; rewrite Fopp_correct. apply Ropp_le_contravar. unfold boundR, boundNat, FtoRradix, FtoR in |- *; simpl in |- *; auto with real zarith. rewrite Rmult_1_l; apply Rlt_le; auto with real zarith arith. apply powerRZ_lt, IZR_lt; lia. Qed.
imports: Reals ZArith List PeanoNat Psatz