proposition: Lemma mxProd_monotone y c (c_le_y : map_mx Bit c <=m y) A B : c <=* A -> c <=* B -> A <=m B -> mxProd y A <=m mxProd y B.
proof: Proof. move=> y'A y'B AB. apply/'forall_forallP => m0 n0. move Hpa' : (mxProd y B m0 n0) => b. case/orP : (letter_split b) Hpa' => [/existsP[b' /eqP -> Hpa']|]. move/'forall_forallP : c_le_y => /(_ ord0 n0); rewrite mxE => c_le_y'. have y'B' : forall i : 'I_m, Bit c ``_ n0 <=l blank_to_star (B i n0). move=> i. by move/'forall_forallP : y'B => /(_ i ord0)/forallP/(_ n0); rewrite !mxE. rewrite (mxProd_Bit c_le_y' y'B' Hpa'). have y'A' : forall i : 'I_m, Bit c ``_ n0 <=l blank_to_star (A i n0). move=> i. by move/'forall_forallP : y'A => /(_ i ord0)/forallP/(_ n0); rewrite !mxE. move Hpa : (mxProd y A m0 n0) => c'. case/orP : (letter_split c') Hpa => [/existsP[c'' /eqP -> Hpa]|Hc' Hpa]. by rewrite (mxProd_Bit c_le_y' y'A' Hpa) lell. rewrite /mxProd !mxE in Hpa Hpa'. case: ifP => Hi in Hpa Hpa'. rewrite (Prod_cons_Bit c_le_y') in Hpa => //. by rewrite -Hpa lell. move=> i. move/'forall_forallP : y'A => /(_ i ord0)/forallP/(_ n0). by rewrite !mxE. apply/hasP; exists (Bit b') => //. move/Prod_Bit: Hpa'. rewrite in_cons => /orP [|]. by rewrite in_cons => ->. move/mapP=> [k Hk Hk']. move/'forall_forallP/(_ k n0): AB. move: Hk'; rewrite mxE => <-; rewrite lel_Bit => /eqP <-. rewrite in_cons; apply/orP; right. apply/mapP; exists k => //; by rewrite mxE. move/'forall_forallP/(_ m0 n0) : AB Hc'. by rewrite Hpa Hpa' lel_Bit => /eqP ->. move=> Hb Hpa'. move: Hpa' Hb. rewrite /mxProd !mxE. case: ifPn => [Hi|Hi <-]. rewrite /Prod. case: ifPn => // H1 <- //; case: ifPn => //; case: ifPn => //; by case: ifPn. by move/'forall_forallP/(_ m0 n0) : AB. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext ssralg_ext num_occ f2 ssrR hamming tanner linearcode