proposition: Lemma mulmx_coker m n (M : 'M_(m, n)) : M *m cokermx M = 0.
proof: Proof. rewrite -{1}[M]mulmx_ebase -!mulmxA mulKVmx ?row_ebase_unit //. by rewrite mul_diag_mx_copid ?mulmx0 // geq_min leqnn orbT. 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