proposition: Lemma det_dvd_step: forall n a (M: 'M[R]_n), (forall i j, a %| M i j) -> a^+n * \det (dvd_step a M) = \det M.
proof: Proof. rewrite /dvd_step => n a M hj. rewrite -detZ; f_equal. apply/matrixP => i j; rewrite !mxE. case: odivrP => [d|h] /=; first by rewrite mulrC. case/dvdrP: (hj i j) => d hd. by move: (h d); rewrite hd eqxx. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype perm choice) mathcomp(matrix bigop zmodp mxalgebra poly polydiv mxpoly) ssrcomplements dvdring minor atomic_operations