proposition: Lemma ltz_divLR m n d : d > 0 -> ((m %/ d)%Z < n) = (m < n * d).
proof: Proof. move=> d_gt0; apply/idP/idP. rewrite -(lezD1 _ n) -(ler_pM2r d_gt0). exact: (Order.POrderTheory.lt_le_trans (ltz_ceil _ _)). rewrite -(ltr_pM2r d_gt0 _ n) //; apply: Order.POrderTheory.le_lt_trans (lez_floor _ _). by rewrite Order.POrderTheory.gt_eqF. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq choice fintype order bigop ssralg) mathcomp(div ssrnum ssrint rat prime path binomial) mathcomp(tuple finset) gaia(fibm)