proposition: Theorem IRNDD_pos : forall r : R, (0 <= r)%R -> (0 <= IRNDD r)%R.
proof: Proof. intros r H1; unfold IRNDD in |- *. generalize (archimed r); intros T; elim T; intros H3 H2; clear T. replace 0%R with (IZR 0); auto with real; apply IZR_le. apply Zle_Zpred. apply lt_IZR; apply Rle_lt_trans with r; auto with real zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz