proposition: Lemma kernel_checksubsum0 (x : 'rV['F_2]_n) : x \notin kernel H -> ((\prod_m0 checksubsum ('V m0) x)%:R = 0)%R.
proof: Proof. move=> x_notin_C. rewrite /C mem_kernel_syndrome0 /syndrome in x_notin_C. have {}x_notin_C : [exists m0, \sum_i (H m0 i) * (x ``_ i) != 0]. rewrite -negb_forall; apply: contra x_notin_C => /forallP x_notin_C. apply/eqP/rowP => a; rewrite !mxE /= -[RHS](eqP (x_notin_C a)). by apply eq_bigr => // i _; rewrite /row_of_tuple !mxE. have {}x_notin_C : [exists m0, \sum_(i in 'V m0) ((H m0 i) * x ``_ i) != 0]. case/existsP : x_notin_C => m0 Hm0. apply/existsP; exists m0. apply: contra Hm0 => /eqP Hm0. apply/eqP. rewrite (bigID [pred i | i \in 'V m0]) /= Hm0 add0r. rewrite [in X in _ = X](_ : 0 = \sum_(i | i \notin 'V m0) 0); last first. by rewrite big_const /= iter_addr0. apply eq_big => n0 //. rewrite VnextE tanner_relE -F2_eq0 => /eqP ->; by rewrite mul0r. have {}x_notin_C : [exists m0, \sum_(i in 'V m0) x ``_ i != 0]. case/existsP : x_notin_C => /= m0 x_notin_C. apply/existsP; exists m0; apply: contra x_notin_C => /eqP H0. apply/eqP; rewrite -[RHS]H0; apply eq_bigr => n0. rewrite VnextE tanner_relE => /eqP ->; by rewrite mul1r. have {}x_notin_C : [exists m0, \sum_(i in 'V m0) x ``_ i != 0]. case/existsP : x_notin_C => /= m0 x_notin_C. by apply/existsP; exists m0; apply: contra x_notin_C => /eqP ->. case/existsP : x_notin_C => m0 Hm0. rewrite /checksubsum (bigID (pred1 m0)) /=. set lhs := (\prod_(i < m | i == m0) _)%nat. suff -> : lhs = O by rewrite mul0n. by rewrite /lhs big_pred1_eq (negbTE Hm0). Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix vector) Reals ssralg_ext ssrR Reals_ext f2 fdist channel tanner linearcode pproba