proposition: Lemma dvdz_mod0P d m : reflect (m %% d = 0)%Z (d %| m)%Z.
proof: Proof. apply: (iffP dvdzP) => [[q ->] | md0]; first by rewrite modzMl. by rewrite (divz_eq m d) md0 addr0; exists (m %/ d)%Z. 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)