proposition: Lemma graph_sumprod_up k (t : tn_tree id' k unit unit) : graph t =2 graph (sumprod_up t).
proof: Proof. move=> a b. move: k t; refine (children_ind _); move=> k t IH. destruct t as [id0 tag0 ch0 up0 down0]; simpl in *. case Ha: (id0 == a). rewrite -map_comp. congr (_ \in _). apply eq_in_map=> i Hi. by destruct i. case Hb: (id0 == b). rewrite -map_comp. congr (_ \in _). apply eq_in_map=> i Hi. by destruct i. elim: ch0 => [|c l IHl] in IH * => //=. rewrite IHl; last first. by move=> t' Ht'; apply IH; rewrite in_cons Ht' orbT. by rewrite IH // in_cons eqxx. 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