fact: Definition ntensmx {m n} (A : 'M_(m, n)) k := nosimpl (if k is k'.+1 return 'M[R]_(m ^ k,n ^ k) then ntensmx_rec A k' else 1).
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop ssralg matrix zmodp div)