proposition: Lemma sum_rowVnextD1_Bit m0 n0 (m0n0 : m0 \in 'F n0) (r : 'rV[letter]_n) : (forall n1, n1 \in 'V m0 :\ n0 -> r ``_ n1 = Bit c ``_ n1) -> Sum (rowVnextD1 r m0 n0) = Bit c ``_ n0.
proof: Proof. move=> H0. rewrite /Sum. case: ifPn => [|Hx]. case/hasP => /= x. case/mapP => /= n1. by rewrite mem_enum => /H0 -> ->. rewrite sum_rowVnextD1_nostars // => *; by rewrite mxE H0. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext ssralg_ext num_occ f2 ssrR hamming tanner linearcode