proposition: Lemma floor_rat : {mono (@ratr F) : x / Num.floor x}.
proof: Proof. move=> x; apply: floor_def; apply/andP; split. - by rewrite -ratr_int ler_rat ge_floor // num_real. - by rewrite -ratr_int ltr_rat lt_succ_floor // num_real. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg countalg div ssrnum) mathcomp(ssrint prime archimedean)