proposition: Lemma row_mx_eq0 (m n1 n2 : nat) (A1 : 'M_(m, n1)) (A2 : 'M_(m, n2)): (row_mx A1 A2 == 0) = (A1 == 0) && (A2 == 0).
proof: Proof. apply/eqP/andP; last by case=> /eqP-> /eqP->; rewrite row_mx0. by rewrite -row_mx0 => /eq_row_mx [-> ->]. 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)