proposition: Lemma select_children_spec s k i j : j \in select_children H s k i = tanner_rel H (id_of_kind k i) (id_of_kind (negk k) j) && (id_of_kind (negk k) j \notin (id_of_kind k i :: s)).
proof: Proof. by destruct k; rewrite /= !mem_filter !mem_ord_enum andbT tanner_relE. 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