fact: Definition Mat : 'M[R]_n := \matrix_(i, j < n) M (enum_val i) (enum_val j).
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat order) mathcomp(fintype bigop ssralg) mathcomp(finset fingroup perm matrix)