proposition: Lemma get_esti_flatten n0 (l : seq (seq (id' * R2))) : get_esti n0 (flatten l) = flatten (map (get_esti n0) l).
proof: Proof. elim: l => [|l0 l] //= IH. by rewrite get_esti_cat 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