proposition: Lemma floor_def x m : m%:~R <= x < (m + 1)%:~R -> floor x = m.
proof: Proof. case/andP=> lemx ltxm1; apply/eqP; rewrite eq_le -!ltzD1. move: (ger_real lemx); rewrite realz => /floor_itv/andP[lefx ltxf1]. by rewrite -!(ltr_int R) 2?(@le_lt_trans _ _ x). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg poly ssrnum ssrint)