proposition: Lemma subseq_labels {A:eqType} {k U P} (l : seq (tn_tree A k U P)) : subseq (map node_id l) (flatten (map labels l)).
proof: Proof. elim: l => [//|a l Hl]. case: a => [id0 tag0 ch0 up0 down0] /=. rewrite eqxx. rewrite -(cat0s [seq node_id i | i <- l]). apply cat_subseq => //; exact: sub0seq. 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