proposition: Lemma floor_ge_int x n : x \is Rreal -> n%:~R <= x = (n <= floor x).
proof: Proof. move=> /floor_itv /andP[lefx ltxf1]; apply/idP/idP => lenx. by rewrite -ltzD1 -(ltr_int R); apply: le_lt_trans ltxf1. by apply: le_trans lefx; rewrite ler_int. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg poly ssrnum ssrint)