proposition: Lemma labels_sumprod_up k (t : tn_tree id' k unit unit) : labels (sumprod_up t) = labels t.
proof: Proof. move: k t; refine (children_ind _); move=> k [id0 tag0 ch0 up0 down0] /= IH. congr (_ :: _). rewrite -map_comp. congr flatten. apply eq_in_map. by move=> t0 H0; 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