proposition: Lemma tech_up : forall (r:R) (z:Z), r < IZR z -> IZR z <= r + 1 -> z = up r.
proof: Proof. intros r z Hlt Hle. destruct (archimed r) as [Hlt'%Ropp_lt_contravar Hle'%Ropp_le_contravar]. apply (Rplus_le_compat_l (- r)) in Hle'. rewrite Ropp_minus_distr, Rminus_def, <-Rplus_assoc, Rplus_opp_l, Rplus_0_l in Hle'. apply Z.sub_move_0_r, one_IZR_lt1; split; rewrite minus_IZR. - replace (-1) with (r + (- r + - 1)) by (now rewrite <-Rplus_assoc, Rplus_opp_r, Rplus_0_l). now apply Rplus_lt_le_compat. - replace 1 with (r + 1 + -r) by (now rewrite (Rplus_comm r), Rplus_assoc, Rplus_opp_r, Rplus_0_r). now apply Rplus_le_lt_compat. Qed.
imports: Rdefinitions Raxioms RIneq ZArith Ztac