proposition: Lemma floor_le : {homo floor : x y / x <= y}.
proof: Proof. move=> x y lexy; move: (floorP x) (floorP y); rewrite (ger_real lexy). case: ifP => [_ /andP[lefx _] /andP[_] | _ /eqP-> /eqP-> //]. by move=> /(le_lt_trans lexy) /(le_lt_trans lefx); rewrite ltr_int ltzD1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg poly ssrnum ssrint)