proposition: Theorem IRNDD_correct3 : forall r : R, (r - 1 < IRNDD r)%R.
proof: Proof. intros r; unfold IRNDD in |- *. generalize (archimed r); intros T; elim T; intros H1 H2; clear T. unfold Z.pred, Rminus in |- *; rewrite plus_IZR; simpl in |- *; auto with real. Qed.
imports: Reals ZArith List PeanoNat Psatz