proposition: Lemma nfloor_ex : forall x : R, 0 <= x -> {n : nat | INR n <= x < INR n + 1}.
proof: Proof. intros. destruct (floor_ex x) as (m,Hm). destruct (Z_lt_le_dec m 0) as [z|z]. apply Zlt_le_succ in z. contradict z. apply Zlt_not_le. apply lt_IZR. apply Rle_lt_trans with (1 := H). rewrite succ_IZR ; apply Hm. destruct m. exists O ; apply Hm. exists (nat_of_P p). rewrite INR_IZR_INZ. rewrite <- Zpos_eq_Z_of_nat_o_nat_of_P. apply Hm. contradict z. apply Zlt_not_le. apply Zlt_neg_0. Qed.
imports: Coq(Reals Psatz ssreflect) Coq(ssrbool) mathcomp(seq)