proposition: Lemma cycle_in_subtree a b s h k i : let t1 := build_tree_rec H rW h (a :: s) k i in uniq_path (tanner_rel H) (id_of_kind k i) (a :: s) -> tanner_rel H a b -> b \in prec_node (a :: s) ++ labels t1 -> b = id_of_kind k i.
proof: Proof. move=> t1 Hun Hgr Hb. have {}Hb : b \in labels t1. rewrite [X in _ \in X ++ _]/= mem_cat in Hb. move /orP: Hb => [] Hb //. rewrite mem_seq1 in Hb. rewrite (eqP Hb) in Hgr. rewrite tanner_relE in Hgr; by destruct a. have [p [Hunp [Hlp _]]] := labels_build_tree_rec Hb Hun. move/acyclic_equiv/(_ (b :: rcons p a)): tanner_acyclic. rewrite /ucycle /ucycleb /cycle. move/andP: Hunp => [Hp Hunp]. rewrite -cat_rcons in Hp Hunp. rewrite -cat1s catA cat_uniq in Hunp. move/andP: Hunp => [] -> _. rewrite cat_path in Hp. rewrite rcons_path last_rcons /=. rewrite Hgr. move/andP: Hp => [] -> _ /=. destruct p; first by []. rewrite size_rcons /=. by move/(_ (eqxx true)). 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