proposition: Lemma tanner_split_uncons (s : seq id') (c x : id') p : c \notin (x :: p) -> path (tanner_split s) x p -> path (tanner_split (c :: s)) x p.
proof: Proof. move: c x s. elim: p => [//|/=y p IHp] c x s Hc /andP[Hx Hp]. rewrite IHp //. move: Hx Hc; rewrite /tanner_split /= 2!(in_cons c). case: ifPn => // /norP[] /negbTE -> /negbTE -> ->. by rewrite 2!in_cons !(eq_sym c) => /norP[/negbTE->] /norP[/negbTE->]. by move /norP/proj2: Hc. 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