proposition: Lemma Minv_uni t : Minv t t = 1.
proof: Proof. have [Muni Mtrig] := unitrigP _ Munitrig. have:= Minvr t t; rewrite eq_refl /= mulr1n => <-. rewrite (bigID (fun v => v <= t)%O) /= [X in _ + X]big1 ?addr0; first last. by move=> v /(contraR (@Mtrig _ _))/eqP ->; rewrite mul0r. rewrite (bigID (fun v => t <= v)%O) /= [X in _ + X]big1 ?addr0; first last. by move=> v /andP[_ /(contraR (@Minv_trig _ _))/eqP->]; rewrite mulr0. rewrite (big_pred1 t) ?Muni ?mul1r // => v /=. by rewrite eq_le. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat order) mathcomp(fintype bigop ssralg) mathcomp(finset fingroup perm matrix)