fact: Definition tanner_split (s : seq id') : rel id' := fun a b => if (a \in s) || (b \in s) then false else tanner_rel H a b.
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