proposition: Lemma mxtens_index_proof m n (ij : 'I_m * 'I_n) : ij.1 * n + ij.2 < m * n.
proof: Proof. case: m ij=> [[[] //]|] m ij; rewrite mulSn addnC -addSn leq_add //. by rewrite leq_mul2r; case: n ij=> // n ij; rewrite leq_ord orbT. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop ssralg matrix zmodp div)