fact: Definition mxProd (y : 'rV[letter]_n) M := \matrix_(i < m, j < n) if i \in 'F j then Prod (colFnextD1 (y ``_ j) (col j M) j i) else M i j.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext ssralg_ext num_occ f2 ssrR hamming tanner linearcode