proposition: Lemma divzMl p m d : p != 0 -> (d %| m -> p * m %/ (p * d) = m %/ d)%Z.
proof: Proof. have [-> | nz_d nz_p] := eqVneq d 0; first by rewrite mulr0 !divz0. by move/divzK=> {1}<-; rewrite mulrCA mulzK ?mulf_neq0. 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)