proposition: Lemma build_tree_full k i a : a \in labels (build_tree_rec H rW #|id'| [::] k i).
proof: Proof. rewrite build_tree_rec_full //. rewrite inE. apply /connectP. move /connectP: (tanner_connected (id_of_kind k i) a) => [p Hp Ha]. by exists p. by rewrite card_sum !card_ord card0 subn0. 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