proposition: Lemma rowV0P m n (A : 'M_(m, n)) : reflect (forall v : 'rV_n, v <= A -> v = 0)%MS (A == 0).
proof: Proof. rewrite -[A == 0]negbK; case: rowV0Pn => IH. by right; case: IH => v svA nzv IH; case/eqP: nzv; apply: IH. by left=> v svA; apply/eqP/idPn=> nzv; case: IH; exists v. 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)