proposition: Lemma mem_rg1_Rfloor x : (range1 (Rfloor x)) x.
proof: Proof. rewrite /range1/mkset. have /andP[_ ->] /= := sup_in_floor_set x. have [|] := pselect ((floor_set x) (Rfloor x + 1)); last first. rewrite /floor_set => /negP. by rewrite negb_and -ltNge rpredD // ?(Rint1, isint_Rfloor). move/ubP : (sup_upper_bound (has_sup_floor_set x)) => h/h. by rewrite gerDl ler10. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra) mathcomp(mathcomp_extra boolp classical_sets set_interval) Setoid