proposition: Lemma ltz_pmod m d : d > 0 -> (m %% d)%Z < d.
proof: Proof. case: m d => n [] // d d_gt0; first by rewrite modz_nat ltz_nat ltn_pmod. by rewrite modNz_nat // -lezD1 addrAC subrK gerDl oppr_le0. 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)