proposition: Lemma floor1_ex : forall x : R, {n : Z | IZR n < x <= IZR n + 1}.
proof: Proof. intros. destruct (floor_ex x) as (n,(Hn1,Hn2)). destruct (Rle_lt_or_eq_dec (IZR n) x Hn1). exists n ; split. apply r. apply Rlt_le, Hn2. exists (Z.pred n) ; rewrite <- e ; split. apply IZR_lt, Zlt_pred. rewrite <- (succ_IZR), <-Zsucc_pred ; apply Rle_refl. Qed.
imports: Coq(Reals Psatz ssreflect) Coq(ssrbool) mathcomp(seq)