proposition: Lemma det_unitrig : \det Mat = 1.
proof: Proof. have [Muni Mtrig] := unitrigP M Munitrig. rewrite /Mat /determinant (bigD1 1%g) //=. rewrite !big1; last by move=> i _; rewrite mxE perm1 Muni. rewrite ?mulr1 ?odd_perm1 ?expr0 ?addr0 //. move=> s Hs. suff [i /eqP Hi] : exists i, M (enum_val i) (enum_val (s i)) == 0. by rewrite (bigD1 i) //= mxE Hi mul0r mulr0. apply/existsP; move: Hs; apply contraR. rewrite negb_exists => /forallP /= H. have {}H : forall i : 'I_n, (enum_val (s i) <= enum_val i)%O. by move=> i; exact: Mtrig (H i). suff Hfix : forall t, s (enum_rank t) = enum_rank t. by apply/eqP/permP => /= i; rewrite perm1 -(enum_valK i); apply: Hfix. elim/ordtype.finord_wf => t IHt. move/(_ (enum_rank t)) : H. rewrite le_eqVlt => /orP[/eqP/(can_inj (@enum_valK _)) // |]. by rewrite enum_rankK => /IHt; rewrite !enum_valK => /perm_inj. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat order) mathcomp(fintype bigop ssralg) mathcomp(finset fingroup perm matrix)