proposition: Lemma unitrig_suml M (Mod : lmodType R) (F : T -> Mod) u : unitrig M -> \sum_(t : T) M u t *: F t = \sum_(t | (t <= u)%O) M u t *: F t.
proof: Proof. move=> /unitrigP[Muni Mtrig]. rewrite (bigID (fun t => (t <= u)%O)) /= addrC big1 ?add0r // => i. by move=> /(contraR (@Mtrig _ _))/eqP ->; rewrite scale0r. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat order) mathcomp(fintype bigop ssralg) mathcomp(finset fingroup perm matrix)