proposition: Lemma mxtens_indexP (m n : nat) (k : 'I_(m * n)) : is_mxtens_index k.
proof: Proof. by rewrite -[k]mxtens_unindexK; constructor. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop ssralg matrix zmodp div)