proposition: Lemma mxtens_index_proof2 m n (k : 'I_(m * n)) : k %% n < n.
proof: Proof. by rewrite ltn_mod; case: n k=> //; rewrite muln0=> [] []. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop ssralg matrix zmodp div)