proposition: Lemma alpha_one_successor n1 m1 d : 'V m1 = [set n1] -> alpha m1 n1 d = (~~ (bool_of_F2 (d ``_ n1)))%:R.
proof: Proof. move=> Vm1. rewrite recursive_computation; last first. by rewrite Vm1 in_set1. rewrite Vm1. rewrite -{1}(setU0 [set n1]) setU1K; last by rewrite in_set0. rewrite rsum_freeon0. rewrite -[X in _ = X]mulR1 checksubsum_set1; congr (_ * _). rewrite big_pred0 // => /= n2. by rewrite in_setD1 in_set1 andNb. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix vector ssrnum) Reals Lra mathcomp(Rstruct) ssrR Reals_ext realType_ext ssr_ext ssralg_ext num_occ bigop_ext fdist channel pproba f2 linearcode subgraph_partition tanner tanner_partition hamming binary_symmetric_channel decoding channel_code summary checksum summary_tanner