proposition: Lemma mulmxKV_kermx m n p (M : 'M_(n, p)) (N : 'M_(m, n)) : N *m M = 0 -> N *m col_ebase M *m kermx M = N.
proof: Proof. rewrite mulmxA mulmxBr mulmx1 mulmxBl mulmxK ?col_ebase_unit //. rewrite -{1}[M]mulmx_ebase !mulmxA. move/(canRL (mulmxK (row_ebase_unit M))); rewrite mul0mx // => BA0. apply: (canLR (addrK _)); rewrite -(pid_mx_id _ _ n (mxrank_leq_col M)) mulmxA. move/eqP: BA0; rewrite /diag_mx /mxrank. by move/(mul_diag_mx_seq_eq0 (@diag_neq0 _ _ M))/eqP ->; rewrite !mul0mx addr0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path tuple) mathcomp(perm fingroup choice ssralg fintype finfun poly polydiv) mathcomp(bigop matrix zmodp mxalgebra) ssrcomplements dvdring mxstructure similar minor binetcauchy stronglydiscrete coherent