proposition: Lemma summxE : forall I r (P : pred I) (E : I -> 'M_(m, n)) i j, (\big[addmx/null_mx]_(k <- r | P k) E k) i j === \sum_(k <- r | P k) E k i j.
proof: Proof. move=> I r P E i j. apply: (big_morph (phi:=fun A => A i j)) => [A B||]. by rewrite/addmx; ring. by rewrite/null_mx; ring. apply radd_morph. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms