proposition: Lemma lel_trans_mat m0 n0 : transitive (@mxlel m0 n0).
proof: Proof. move=> A B C /'forall_forallP /= H1 /'forall_forallP H2. apply/'forall_forallP => m1 n1; by apply: (lel_trans (H1 _ _) (H2 _ _)). Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext ssralg_ext num_occ f2 ssrR hamming tanner linearcode