proposition: Lemma dvd_ker k m0 m1 m2 (M : 'M[R]_(m0,m2)) (N : 'M[R]_(m1,m2)) (X : 'M_(k, m1)) : (M.-ker N %| X) = (M %| X *m N).
proof: Proof. apply/dvdmxP/dvdmxP. move=> [Y ->]; exists (- (Y *m lsubmx (ker (col_mx M N)))). apply/eqP; rewrite mulNmx -addr_eq0 addrC -!mulmxA -mulmxDr -mul_row_col. by rewrite hsubmxK kerK mulmx0. case=> [Y /eqP]; rewrite eq_sym -subr_eq0 -mulNmx -mul_row_col. move=> /kerP [Z /(congr1 rsubmx)]; rewrite row_mxKr -mulmx_rsub => HZ. by exists (-Z); rewrite mulNmx -HZ opprK. 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