fact: Definition unitrig M := [forall t, M t t == 1] && [forall t, [forall (u | M u t != 0), (t <= u)%O]].
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat order) mathcomp(fintype bigop ssralg) mathcomp(finset fingroup perm matrix)