proposition: Lemma unitrig_sumrV M (Mod : lmodType R) (F : T -> Mod) t : unitrig M -> \sum_(u : T) M t u *: F u = \sum_(u | (u <= t)%O) M t u *: F u.
proof: Proof. move=> /unitrigP[Muni Mtrig]. rewrite (bigID (fun u => (u <= t)%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)