proposition: Lemma floorQ_divn (m : nat) (n : nat) : floorQ (m%:Q / n.+1%:Q) = floorQ (m %/ n.+1)%N%:Q.
proof: Proof. apply/esym/floorQ_unique. rewrite -floorQ_int ler_pdivlMr ?ltr_pdivrMr ?ltr0z //. rewrite -!natrM ler_nat ltr_nat mulnDl mul1n. by rewrite [m in (_ <= m < _)%N](divn_eq m n.+1) leq_addr ltn_add2l ltn_mod. Qed.
imports: mathcomp(all_ssreflect all_algebra)