proposition: Lemma sum_lfunE I (r : seq I) (P : pred I) (fs : I -> 'Hom(aT, rT)) x : (\sum_(i <- r | P i) fs i) x = \sum_(i <- r | P i) fs i x.
proof: Proof. by elim/big_rec2: _ => [|i _ f _ <-]; rewrite lfunE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)