proposition: Lemma mxProd_Bit (y : 'rV[letter]_n) n0 (c : 'F_2) (cy : Bit c <=l y ``_ n0) (A : 'M[letter]_(m, n)) : (forall i, Bit c <=l blank_to_star (A i n0)) -> forall m0 b, mxProd y A m0 n0 = Bit b -> b = c.
proof: Proof. move=> Ha m0 b. rewrite /mxProd mxE. case: ifP => m0n0. move/Prod_Bit => mem_b. have Ha' : forall i : 'I_m, Bit c <=l blank_to_star ((col n0 A) i ord0). move=> i; move: Ha => /(_ i); by rewrite !mxE. apply: (@Bit_col _ _ _ cy _ ('F n0 :\ m0) Ha'). move: mem_b; rewrite inE; case/orP => [/eqP <-|mem_b]. by rewrite eqxx. apply/orP; right. case/mapP : mem_b => x Hx Hx'. apply/mapP; by exists x. by move=> Hf; move: Ha => /(_ m0); rewrite Hf lel_Bit => /eqP[]. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext ssralg_ext num_occ f2 ssrR hamming tanner linearcode