proposition: Lemma mxtens_unindexK m n : cancel (@mxtens_unindex m n) (@mxtens_index m n).
proof: Proof. case: m=> [[[] //]|m]. case: n=> [|n] k. by suff: False by []; move: k; rewrite muln0=> [] []. by apply: val_inj=> /=; rewrite -divn_eq. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop ssralg matrix zmodp div)