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