proposition: Lemma tanner_split_cons c s : subrel (tanner_split (c :: s)) (tanner_split s).
proof: Proof. rewrite /subrel /tanner_split /= => a b. rewrite in_cons in_cons. case Ha: (a \in s); first by rewrite /= orbT. case Hb: (b \in s); first by rewrite /= orbT orbT. by case: ifP. 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