proposition: Lemma floor_le x : (floor x)%:~R <= x.
proof: Proof. by rewrite -RfloorE; exact: Rfloor_le. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra) mathcomp(mathcomp_extra boolp classical_sets set_interval) Setoid