proposition: Lemma divzMA m n p : (n * p %| m -> m %/ (n * p) = (m %/ n)%Z %/ p)%Z.
proof: Proof. have [-> | nz_p] := eqVneq p 0; first by rewrite mulr0 !divz0. have [-> | nz_n] := eqVneq n 0; first by rewrite mul0r !divz0 div0z. by move/divzK=> {2} <-; rewrite mulrA mulrAC !mulzK. 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)