proposition: Lemma dvd_mx_col k m0 m1 m2 (M : 'M[R]_(m0,m2)) (N : 'M[R]_(m1,m2)) (X : 'M_(k, m2)) : (X %| col_mx M N) = (X %| M) && (X %| N).
proof: Proof. apply/dvdmxP/andP=> [[Y]|[/dvdmxP [M' ->] /dvdmxP [N' ->]]]; last first. by exists (col_mx M' N'); rewrite mul_col_mx. rewrite -[Y]vsubmxK mul_col_mx => HY. have := (congr1 usubmx HY, congr1 dsubmx HY). by rewrite !col_mxKu !col_mxKd => [[-> ->]]; rewrite !dvdmxMl. 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