proposition: Lemma matrix_sum_delta A : A = \sum_(i < m) \sum_(j < n) A i j *: delta_mx i j.
proof: Proof. apply/matrixP=> i j. rewrite summxE (bigD1_ord i) // summxE (bigD1_ord j) //= !mxE !eqxx mulr1. rewrite !big1 ?addr0 //= => [i' | j'] _. by rewrite summxE big1// => j' _; rewrite !mxE eq_liftF mulr0. by rewrite !mxE eqxx eq_liftF mulr0. 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)