proposition: Lemma floor_ex : forall x : R, {n : Z | IZR n <= x < IZR n + 1}.
proof: Proof. intros. exists (up (x-1)) ; split. assert (Rw : x = 1 + (x-1)) ; [ring | rewrite {2}Rw => {Rw}]. assert (Rw :IZR (up (x - 1)) = (IZR (up (x - 1)) - (x - 1)) + (x-1)) ; [ring | rewrite Rw ; clear Rw]. apply Rplus_le_compat_r, (proj2 (archimed _)). assert (Rw : x = (x-1) + 1) ; [ring | rewrite {1}Rw ; clear Rw]. apply Rplus_lt_compat_r, (proj1 (archimed _)). Qed.
imports: Coq(Reals Psatz ssreflect) Coq(ssrbool) mathcomp(seq)