proposition: Lemma enum_id_ok (a : id') : a \in enum_id.
proof: Proof. rewrite /enum_id mem_cat. apply /orP. destruct a; [left | right]; apply /map_f/my_ord_enum_ok. 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