proposition: Lemma sub_kermxP p m n (A : 'M_(m, n)) (B : 'M_(p, m)) : reflect (B *m A = 0) (B <= kermx A)%MS.
proof: Proof. apply: (iffP submxP) => [[D ->]|]; first by rewrite -mulmxA mulmx_ker mulmx0. by move/mulmxKV_ker; exists (B *m col_ebase A). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup perm order) mathcomp(div prime binomial ssralg finalg zmodp matrix)