proposition: Lemma divzA m n p : (p %| n -> n %| m * p -> m %/ (n %/ p)%Z = m * p %/ n)%Z.
proof: Proof. move/divzK=> p_dv_n; have [->|] := eqVneq n 0; first by rewrite div0z !divz0. rewrite -{1 2}p_dv_n mulf_eq0 => /norP[pn_nz p_nz] /divzK; rewrite mulrA p_dv_n. by move/mulIf=> {1} <- //; rewrite 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)