proposition: Theorem IRNDD_correct1 : forall r : R, (IRNDD r <= r)%R.
proof: Proof. intros r; unfold IRNDD in |- *. generalize (archimed r); intros T; elim T; intros H1 H2; clear T. unfold Z.pred in |- *; apply Rplus_le_reg_l with (1 + - r)%R. ring_simplify (1 + - r + r)%R. apply Rle_trans with (2 := H2). rewrite plus_IZR; right; simpl in |- *; ring. Qed.
imports: Reals ZArith List PeanoNat Psatz