proposition: Lemma enum_select_children s k i : enum (select_children H s k i) = select_children H s k i.
proof: Proof. by destruct k; rewrite /= /enum_mem unlock /=; apply eq_filter => j; rewrite !inE mem_filter !in_cons mem_ord_enum andbT. 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