proposition: Lemma sup_in_floor_set x : (floor_set x) (sup (floor_set x)).
proof: Proof. have /(sup_adherent ltr01) [y Fy] := has_sup_floor_set x. have /sup_upper_bound /ubP /(_ _ Fy) := has_sup_floor_set x. rewrite le_eqVlt=> /orP[/eqP<-//| lt_yFx]. rewrite ltrBlDr -ltrBlDl => lt1_FxBy. pose e := sup (floor_set x) - y; have := has_sup_floor_set x. move/sup_adherent=> -/(_ e) []; first by rewrite subr_gt0. move=> z Fz; rewrite /e opprB addrCA subrr addr0 => lt_yz. have /sup_upper_bound /ubP /(_ _ Fz) := has_sup_floor_set x. rewrite -(lerD2r (-y)) => /le_lt_trans /(_ lt1_FxBy). case/andP: Fy Fz lt_yz=> /RintP[yi -> _]. case/andP=> /RintP[zi -> _]; rewrite -rmorphB /= ltrz1 ltr_int. rewrite lt_neqAle => /andP[ne_yz le_yz]. rewrite -[_-_]gez0_abs ?subr_ge0 // ltz_nat ltnS leqn0. by rewrite absz_eq0 subr_eq0 eq_sym (negbTE ne_yz). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra) mathcomp(mathcomp_extra boolp classical_sets set_interval) Setoid