proposition: Lemma dvdmxP m n l (M : 'M[R]_(m, n)) (B : 'M_(l, n)) : reflect (exists X, B = X *m M) (M %| B).
proof: Proof. apply: (iffP eqP)=> [<-|[X -> {B}]]; first by eexists. elim: n => //= [|n ihn] in m l M X *; first by apply/matrixP => i []. rewrite -[n.+1]/(1 + n)%N in M X *. set Ml := lsubmx M; set K := ker _; set W := divid _ _; set k := dim_ker _. rewrite mulmxDl -mulmxA -!mulmx_rsub -!mulmxBl; apply: canLR (@addrNK _ _) _. set Mr := rsubmx M; rewrite -mulmxBl -[M]hsubmxK -/Mr -/Ml !mul_mx_row. have /kerP [Y ->] : (X - W) *m Ml == 0. by rewrite mulmxBl dividK -mulmx_lsub ?subrr ?subidMl. by rewrite -!mulmxA !kerK !mulmx0 ihn. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype perm choice matrix bigop zmodp mxalgebra poly) ssrcomplements dvdring stronglydiscrete