proposition: Lemma sum_rowVnextD1 (c : 'rV['F_2]_n) (r : 'rV[letter]_n) m0 n0 : (forall j : 'I_n, j \in 'V m0 :\ n0 -> r ``_ j = Bit (c ``_ j)) -> sum_letter (filter is_Bit (rowVnextD1 r m0 n0)) = \sum_(i0 in 'V m0 :\ n0) c ``_ i0.
proof: Proof. move=> H0. rewrite /sum_letter big_filter big_map big_mkcond /= big_filter. apply eq_bigr => n1 Hn1; by rewrite H0. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext ssralg_ext num_occ f2 ssrR hamming tanner linearcode