proposition: Lemma dvd0mx k m n (M : 'M[R]_(m,n)) : ((0 : 'M[R]_(k,n)) %| M) = (M == 0).
proof: Proof. by apply/idP/eqP => [/dvdmxP [X ->]|-> //]; rewrite 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