proposition: Lemma for_base_fp : forall r:R, IZR (up r) - r > 0 /\ IZR (up r) - r <= 1.
proof: Proof. intro; split; cut (IZR (up r) > r /\ IZR (up r) - r <= 1). - intro; elim H; intros. apply (Rgt_minus (IZR (up r)) r H0). - apply archimed. - intro; elim H; intros. exact H1. - apply archimed. Qed.
imports: Rdefinitions Raxioms RIneq ZArith Ztac