proposition: Lemma mxtens_indexK m n : cancel (@mxtens_index m n) (@mxtens_unindex m n).
proof: Proof. case: m=> [[[] //]|m]; case: n=> [[_ [] //]|n]. move=> [i j]; congr (_, _); apply: val_inj=> /=. by rewrite divnMDl // divn_small ?addn0. by rewrite modnMDl // modn_small. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop ssralg matrix zmodp div)