proposition: Lemma post_prob_uniform_checksubsum (x : 'rV['F_2]_n) : (`U HC) `^^ W (x | y) = (post_prob_uniform_cst [set cw in C] y * (\prod_m0 (\delta ('V m0) x))%:R * W ``(y | x))%R.
proof: Proof. rewrite post_prob_uniform_kernel; congr (_ * _ * _)%R. by rewrite big_morph_natRM checksubsum_in_kernel inE mem_kernel_syndrome0. 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