proposition: Lemma floorQ_div (q : rat) (m : nat) : floorQ (q / m.+1%:Q) = floorQ ((floorQ q)%:Q / m.+1%:Q).
proof: Proof. apply/floorQ_unique; move: (floorQ_spec q) (floorQ_spec (q / m.+1%:Q)). rewrite !ler_pdivlMr ?ltr_pdivrMr ?ltr0z // intrD -intrM ler_int. move=> /andP[_ Hq] /andP[Hdiv /le_lt_trans ->] //. by rewrite -ltzD1 -(ltr_int rat) intrD (le_lt_trans Hdiv). Qed.
imports: mathcomp(all_ssreflect all_algebra)