proposition: Lemma Minv_trig t u : Minv u t != 0 -> (t <= u)%O.
proof: Proof. have [Muni Mtrig] := unitrigP _ Munitrig. apply contraR => H; apply/eqP; elim/ordtype.finord_wf: u H => /= u IHu Hu. have:= Minvr u t. rewrite [X in _ = (nat_of_bool X)%:R](_ : _ = false) /=; first last. by apply negbTE; move: Hu; apply contra => /eqP->. rewrite (bigID (fun v => v <= u)%O) /= [X in _ + X]big1 ?addr0; first last. by move=> v /(contraR (@Mtrig _ _)) /eqP ->; rewrite mul0r. rewrite (bigD1 u) //= Muni mul1r big1 ?addr0 // => i /andP[Hneq Hlt]. rewrite IHu ?mulr0 //. - by rewrite lt_neqAle Hlt Hneq. - by move: Hu; apply contra => /le_trans; apply. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat order) mathcomp(fintype bigop ssralg) mathcomp(finset fingroup perm matrix)