proposition: Lemma Minv_unitrig : unitrig Minv.
proof: Proof. apply/unitrigP; split; [exact: Minv_uni | exact: Minv_trig]. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat order) mathcomp(fintype bigop ssralg) mathcomp(finset fingroup perm matrix)