proposition: Lemma kernel_checksubsum (x : 'rV['F_2]_n) : x \in kernel H = \big[andb/true]_m0 checksubsum ('V m0) x.
proof: Proof. apply/idP/idP; last first. apply: contraTT => /kernel_checksubsum0. rewrite -(@big_morph _ _ nat_of_bool true muln true andb) //. rewrite -eqb0 /= (_ : 0 = 0%:R)%R //; by move/INR_eq/eqP. move=> ? ? /=; by rewrite mulnb. move/kernel_checksubsum1. rewrite -(@big_morph _ _ nat_of_bool true muln true andb) //; last first. move=> ? ? /=; by rewrite mulnb. rewrite (_ : 1 = true%:R)%R // => /INR_eq/esym. by case: (\big[andb/true]_(_ < _) _). 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