proposition: Lemma labels_sumprod_down k (t : tn_tree id' k R2 unit) dn : labels (sumprod_down t dn) = labels t.
proof: Proof. move: k t dn; refine (children_ind _). move=> k [id0 tag0 ch0 up0 down0] /= IH dn. destruct (push_init dn); simpl. f_equal. rewrite -(map_apply_seq_eq (g:=labels)) //; last first. by rewrite size_seqs_but1 size_map. move=> c cl Hc. by rewrite 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