proposition: Lemma rmul_foldr_rsum {I A} {X : finType} (a : R) (g : I -> X -> A -> A) (F0 : A -> R) l d : a * foldr (fun n1 (F : A -> R) t => \sum_(x in X) F (g n1 x t)) F0 l d = foldr (fun n1 (F : A -> R) t => \sum_(x in X) F (g n1 x t)) (fun t => a * F0 t) l d.
proof: Proof. elim: l d => [|x l IH] d //=. rewrite big_distrr. apply eq_bigr => i Hi. apply IH. 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