proposition: Lemma int_floor x : exists m : int, floor x == m.
proof: Proof. case: (range1_floor x); set y := floor x => leyx ltxy1; pose h2 : R := 2^-1. have h2gt0: 0 < h2 by apply: invR_gt0. have lty2y: y - h2 < y by rewrite -subR_ge0 addRC addKR -oppR0 leR_opp2. have [[_ [m lemx] ley2m] | //] := sup_total (y - h2) (nonempty_floor_set x). rewrite -/intRR in lemx ley2m; exists m; split; last exact: sup_ub. pose m2 := m + h2; have leym2: y <= m2 by rewrite -(leR_add2r (- h2)) addRK. apply: sup_le_ub => // _ [m1 lem1x]; rewrite -(leR_add2r 1) -!intRD1. apply/intR_leP/intR_ltP; have:= h2gt0; rewrite -(leR_add2l m2) addR0. rewrite -addRA -mul2R (divRR (gtR_neq ltR02)) -(intRD1 m). exact/leR_lt_trans/(ge_sup_ub _ leym2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div order) mathcomp(ssralg ssrnum ssrint rat intdiv) Coq(Morphisms Setoid) fourcolor(real realsyntax)