proposition: Lemma floorQ_spec (r : rat) : (floorQ r)%:Q <= r < (floorQ r)%:Q + 1.
proof: Proof. rewrite -[r in _ <= r < _]divq_num_den ler_pdivlMr ?ltr_pdivrMr ?ltr0z //. by rewrite -rat1 -intrD -!intrM ler_int ltr_int lez_floor ?ltz_ceil. Qed.
imports: mathcomp(all_ssreflect all_algebra)