proposition: Lemma rowE m n i (A : 'M_(m, n)) : row i A = delta_mx 0 i *m A.
proof: Proof. apply/rowP=> j; rewrite !mxE (bigD1_ord i) //= mxE !eqxx mul1r. by rewrite big1 ?addr0 // => i'; rewrite mxE /= lift_eqF mul0r. 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)