proposition: Lemma lell_mat m0 n0 (A : 'M[letter]_(m0, n0)) : A <=m A.
proof: Proof. rewrite /mxlel; apply/'forall_forallP => i j; exact: lell. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext ssralg_ext num_occ f2 ssrR hamming tanner linearcode