proposition: Lemma up_sumprod_down dn {k} (t : tn_tree id' k R2 unit) : up (sumprod_down t dn) = up t.
proof: Proof. destruct t; simpl. by destruct (push_init dn). 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