proposition: Lemma unitrig_sum1r M (Mod : lmodType R) (F : T -> Mod) t : unitrig M -> \sum_(u : T) M u t *: F u = F t + \sum_(u | (t < u)%O) M u t *: F u.
proof: Proof. move=> Hut; rewrite unitrig_sumr // (bigD1 t) //=. move: Hut => /unitrigP[-> _]; rewrite scale1r; congr (_ + _). by apply eq_bigl => u; rewrite lt_def andbC. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat order) mathcomp(fintype bigop ssralg) mathcomp(finset fingroup perm matrix)