proposition: Lemma unique_children h s k i : uniq [seq node_id (sumprod_up (build_tree_rec H rW h (id_of_kind k i :: s) _ j)) | j <- select_children H s k i].
proof: Proof. rewrite map_inj_uniq. by rewrite uniq_select_children. move=> x y /=. rewrite !node_id_sumprod_up !node_id_build. by apply id_of_kind_inj. 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