proposition: Lemma mxSumProd_monotone A B y (c : 'rV['F_2]_n) (c_le_y : map_mx Bit c <=m y) : c <=* A -> c <=* B -> A <=m B -> mxSumProd y A <=m mxSumProd y B.
proof: Proof. move => Ha Ha' Haa'. apply/'forall_forallP => m0 n0. rewrite /mxSumProd !mxE. case: ifP => Hi. rewrite /Sum. case: ifPn => [Hn1 | _]. case: ifPn => // /negP Hn2. exfalso; apply Hn2; move: Hn1. exact/has_starblank_rowVnextD1/(mxProd_monotone c_le_y). case: ifPn => // Hn2. apply/orP; left. apply/eqP; congr Bit. rewrite /sum_letter 2!big_filter 2!big_map [in LHS]big_mkcond /=. rewrite [in RHS]big_mkcond /= 2!big_filter; apply eq_bigr => i Hi'. rewrite 2![(row _ _) _ _]mxE. move/forallP/(_ m0)/forallP/(_ i): (mxProd_monotone c_le_y Ha Ha' Haa') => /orP [/eqP -> //|]. move: Hn2. move HB : (mxProd y A m0 i) => a. case/letterP : a HB => //= _ Hn2 /eqP. by move=> -> /=. move=> abs. exfalso. move/negP : Hn2; apply. apply/hasP; exists Star => //. apply/mapP; exists i => //. by rewrite mem_enum. by rewrite mxE. rewrite Hi. move/'forall_forallP : Haa'; by apply. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext ssralg_ext num_occ f2 ssrR hamming tanner linearcode