proposition: Lemma lez_div m d : (`|(m %/ d)%Z| <= `|m|)%N.
proof: Proof. wlog d_gt0: d / d > 0; last case: d d_gt0 => // d d_gt0. by move=> IH; case/intP: d => [|n|n]; rewrite ?divz0 ?divzN ?abszN // IH. case: m => n; first by rewrite divz_nat leq_div. by rewrite divNz_nat // NegzE !abszN ltnS leq_div. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime order) mathcomp(ssralg poly ssrnum ssrint archimedean rat matrix) mathcomp(polydiv perm zmodp mxalgebra vector)