proposition: Lemma approx_mxSumProd M : c <=* M -> c <=* mxSumProd y M.
proof: Proof. move=> cA. apply/'forall_forallP => /= m0 k; rewrite {k}(ord1 k). apply/forallP=> /= j. rewrite 4!mxE. case: ifPn => m0Fj; last first. rewrite mxE (negbTE m0Fj). move/'forall_forallP/(_ m0 ord0) : cA => /forallP/(_ j). by rewrite 3!mxE. rewrite /Sum. case: ifPn => // nostars. apply/orP; left; apply/eqP; congr Bit. rewrite (sum_rowVnextD1_nostars Hc) //= => n1 Hn1. rewrite mxE. move Hia : (mxProd y M m0 n1) => b. case/orP : (letter_split b) Hia => [/existsP[/= b' /eqP -> Hia]|Hb Hia]. move/'forall_forallP : c_le_y => /(_ ord0 n1); rewrite !mxE => c_le_y'. have Ha' : forall i : 'I_m, Bit c ``_ n1 <=l blank_to_star (M i n1). move=> i. by move/'forall_forallP : cA => /(_ i ord0)/forallP/(_ n1); rewrite !mxE. by rewrite (mxProd_Bit c_le_y' Ha' Hia). move: nostars. rewrite -all_predC. move/allP => /=. move/(_ b). have X : b \in rowVnextD1 (row m0 (mxProd y M)) m0 j. rewrite -Hia. apply/mapP => /=. exists n1 => //; by rewrite ?(mxE, mem_enum). move/(_ X). by rewrite Hb. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext ssralg_ext num_occ f2 ssrR hamming tanner linearcode