proposition: Lemma curry_mxvec_bij : {on 'I_(m * n), bijective (uncurry mxvec_index)}.
proof: Proof. exists (enum_val \o cast_ord (esym mxvec_cast)) => [[i j] _ | k _] /=. by rewrite cast_ordK enum_rankK. by case/mxvec_indexP: k => i j /=; rewrite cast_ordK enum_rankK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup perm order) mathcomp(div prime binomial ssralg countalg finalg zmodp)