proposition: Lemma sum_rowVnextD1_nostars m0 n0 (r : 'rV[letter]_n) : (forall j, j \in 'V m0 :\ n0 -> r ``_ j = Bit (c ``_ j)) -> m0 \in 'F n0 -> let s := rowVnextD1 r m0 n0 in ~~ has starblank s -> sum_letter (filter is_Bit s) = c ``_ n0.
proof: Proof. move=> H0 m0n0 s starblank. move/matrixP/(_ ord0 m0) : Hc. rewrite !mxE (bigD1 n0) //= => Hc'. set rhs := \sum_(_ < _ | _) _ in Hc'. have Hrhs : rhs = \sum_(i0 < _ | i0 \in 'V m0 :\ n0) c ``_ i0. rewrite /rhs. transitivity (\sum_(H0 < n | (H0 != n0) && (m0 \in 'F H0)) H m0 H0 * c^T H0 ord0). rewrite (bigID (fun j => m0 \in 'F j)) /=. rewrite (_ : \sum_(i0 < n | (i0 != n0) && (m0 \notin 'F i0)) H m0 i0 * c^T i0 ord0 = 0). by rewrite addr0. rewrite (eq_bigr (fun=> 0)). by rewrite big_const /= iter_addr0. move=> /= i0 /andP[] i0j. rewrite FnextE VnextE tanner_relE -F2_eq0 => /eqP ->; by rewrite mul0r. apply eq_big. by move=> j0 /=; rewrite in_setD1 FnextE. move=> i0 /andP[] H1. rewrite FnextE VnextE tanner_relE => /eqP ->; by rewrite mul1r mxE. rewrite Hrhs (_ : H _ _ = 1) ?mul1r ?mxE in Hc'; last first. move: m0n0; by rewrite FnextE VnextE tanner_relE => /eqP. move/eqP : Hc'. rewrite addr_eq0 => /eqP ->. rewrite (@sum_rowVnextD1 c) ?oppr_char2 // => *; 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