proposition: Theorem boundRCorrect1 : forall r : R, (r < boundR r)%R.
proof: Proof. intros r; case (Rle_or_lt r 0); intros H'. apply Rle_lt_trans with (1 := H'). unfold boundR, boundNat, FtoRradix, FtoR in |- *; simpl in |- *; auto with real. rewrite Rmult_1_l; auto with real zarith. apply powerRZ_lt, IZR_lt; lia. apply Rlt_trans with (2 := boundNatCorrect (Z.abs_nat (up (Rabs r)))). replace (Rabs r) with r; auto with real. apply Rlt_le_trans with (r2 := IZR (up r)); auto with real zarith. case (archimed r); auto. apply IZR_le, Zle_abs. unfold Rabs in |- *; case (Rcase_abs r); auto with real. intros H'0; contradict H'0; auto with real. Qed.
imports: Reals ZArith List PeanoNat Psatz