proposition: Lemma up_tech : forall (r:R) (z:Z), IZR z <= r -> r < IZR (z + 1) -> (z + 1)%Z = up r.
proof: Proof. intros. apply tech_up with (1 := H0). rewrite plus_IZR. now apply Rplus_le_compat_r. Qed.
imports: Rdefinitions Raxioms RIneq ZArith Ztac