proposition: Lemma mxSumProd_invariant A : c <=* A -> mxSumProd y A <=m A -> c <=* mxSumProd y (mxSumProd y A) && mxSumProd y (mxSumProd y A) <=m mxSumProd y A.
proof: Proof. move=> Hap Halpha. have Hap' := approx_mxSumProd Hap. have Hap'' := approx_mxSumProd Hap'. rewrite Hap'' /=. by apply (mxSumProd_monotone c_le_y). Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext ssralg_ext num_occ f2 ssrR hamming tanner linearcode