proposition: Lemma range1_floor x : range1 (floor x) x.
proof: Proof. by split; [apply: sup_le_ub | apply: has_floor_max]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div order) mathcomp(ssralg ssrnum ssrint rat intdiv) Coq(Morphisms Setoid) fourcolor(real realsyntax)