proposition: Lemma nz_row_eq0 m n (A : 'M_(m, n)) : (nz_row A == 0) = (A == 0).
proof: Proof. rewrite /nz_row; symmetry; case: pickP => [i /= nzAi | Ai0]. by rewrite (negPf nzAi); apply: contraTF nzAi => /eqP->; rewrite row0 eqxx. by rewrite eqxx; apply/eqP/row_matrixP=> i; move/eqP: (Ai0 i) ->; rewrite row0. 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 countalg finalg zmodp)