proposition: Lemma det_dvd_step_tool : forall m n a (M N: 'M[R]_(m,n)), M = a *: N -> forall i j, a %| M i j.
proof: Proof. move => m n a M N /matrixP h i j. rewrite (h i j) !mxE mulrC. by apply/dvdr_mull/dvdrr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path ssralg) mathcomp(fintype perm choice matrix bigop zmodp poly polydiv mxpoly) CoqEAL(ssrcomplements minor dvdring) polydvd