proposition: Theorem IRNDD_correct2 : forall r : R, (r < Z.succ (IRNDD r))%R.
proof: Proof. intros r; unfold IRNDD in |- *. generalize (archimed r); intros T; elim T; intros H1 H2; clear T. rewrite <- Zsucc_pred; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz