fact: Definition mxlel m n (A B : 'M[letter]_(m, n)) := [forall m, [forall n, A m n <=l B m n]].
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext ssralg_ext num_occ f2 ssrR hamming tanner linearcode