proposition: Lemma lelmxStar : mxSumProd H y (mxStar H) <=m mxStar H.
proof: Proof. apply/'forall_forallP => m0 n0; rewrite !mxE. case: ifP => m0n0 /=; first exact: le_Sum_Star. by rewrite m0n0 /= lell. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext ssralg_ext num_occ f2 ssrR hamming tanner linearcode