proposition: Lemma unitrigP M : reflect ((forall t, M t t = 1) /\ (forall t u, M u t != 0 -> (t <= u)%O)) (unitrig M).
proof: Proof. apply/(iffP andP) => [[/forallP Huni /forallP Htrig] | [Huni Htrig]]. - split => [t | t u]; first by apply/eqP. by have:= Htrig t => /forall_inP; apply. - split; apply/forallP => t; first by rewrite Huni. by apply/forall_inP; apply Htrig. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat order) mathcomp(fintype bigop ssralg) mathcomp(finset fingroup perm matrix)