proposition: Lemma sub_kermxP p m n (A : 'M_(m, n)) (B : 'M_(p, m)) : reflect (B *m A = 0) (ker A %| B).
proof: Proof. apply: (iffP (dvdmxP _ _)); last by move=> /eqP /kerP [X ->]; eexists. by case=> D ->; rewrite -mulmxA kerK mulmx0. 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