proposition: Lemma beta_one_successor n1 m1 d : 'F n1 = [set m1] -> beta n1 m1 d = W (d ``_ n1) (y ``_ n1).
proof: Proof. move=> Fn1. rewrite /beta -[X in _ = X]mulR1. congr (_ * _). set g := BIG_F. transitivity (\prod_(i in set0) g i). apply eq_bigl => /= m2. rewrite Fn1 in_setD1 in_set1 in_set0. by case: (m2 == m1). by rewrite big_set0. 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