proposition: Lemma beta_map {A} F w (l : seq A) : beta w (map F l) = beta_op w (\big[beta_op/(R1,R1)]_(i <- l) F i).
proof: Proof. by rewrite /beta foldlE /= big_cons big_map. Qed.
imports: Wf_nat Init.Wf Recdef Reals mathcomp(all_ssreflect perm zmodp matrix ssralg) mathcomp(Rstruct) ssrR Reals_ext ssr_ext ssralg_ext bigop_ext f2 fdist channel pproba linearcode subgraph_partition tanner tanner_partition summary ldpc checksum ldpc_algo