proposition: Lemma nfloor1_ex : forall x : R, 0 < x -> {n : nat | INR n < x <= INR n + 1}.
proof: Proof. intros. destruct (nfloor_ex x (Rlt_le _ _ H)) as (n,(Hn1,Hn2)). destruct (Rle_lt_or_eq_dec (INR n) x Hn1). exists n ; split. apply r. apply Rlt_le, Hn2. destruct n. contradict H. rewrite <- e ; simpl ; apply Rlt_irrefl. exists n ; rewrite <- e ; split. apply lt_INR, Nat.lt_succ_diag_r. rewrite <- (S_INR) ; apply Rle_refl. Qed.
imports: Coq(Reals Psatz ssreflect) Coq(ssrbool) mathcomp(seq)