proposition: Lemma summxE I r (P : pred I) (E : I -> 'M_(m, n)) i j : (\sum_(k <- r | P k) E k) i j = \sum_(k <- r | P k) E k i j.
proof: Proof. by apply: (big_morph (fun A => A i j)) => [A B|]; rewrite mxE. 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)