proposition: Lemma tanner_rel_split (s : seq id') (x : id') p : ~~has (mem s) (x::p) -> path (tanner_rel H) x p -> path (tanner_split s) x p.
proof: Proof. move: x s. elim: p => //= y p IHp x s Hs /andP[Hx Hp]. rewrite IHp //. rewrite /tanner_split Hx. by case/norP: Hs => /negbTE -> /norP[] /negbTE ->. by case/norP: Hs. 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