proposition: Fact nonempty_floor_set x : Real.nonempty (floor_set x).
proof: Proof. have [le0x | lex0] := leR_total 0 x; first by exists 0%N. have ub_nx0: Real.has_sup (floor_set (- x)). by split=> //; exists 0%N; split; rewrite -leR_opp2 oppRK oppR0. have [[_ [m _] lexm] | /ltPR//] := sup_total (floor (- x) - 1) (proj1 ub_nx0). pose m1 := (m + 1)%R; pose m2 := (m1 + 1)%R. exists (- m2)%R; split; move: lexm; rewrite -/intRR -(addRK m 1) leR_add2r. rewrite -{2}(oppRK x) intRN leR_opp2 -{2}(subRK (- x) 1) !intRD1 leR_add2r. apply/leR_trans/ltRW; rewrite -(leR_add2r 1) subRK. by apply: has_floor_max; case: ub_nx0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div order) mathcomp(ssralg ssrnum ssrint rat intdiv) Coq(Morphisms Setoid) fourcolor(real realsyntax)