fact: Fixpoint mypath (h : nat) : seq (seq id') := match h with | 0 => [::] | S h' => let ll := [::] :: mypath h' in flatten [seq [seq i :: l | l <- ll & path myrel i l] | i <- enum_id] end.
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