proposition: Lemma build_tree_rec_sound h s k i a b : graph (build_tree_rec H rW h s k i) a b -> tanner_rel H a b.
proof: Proof. move: h s k i a b. elim => [|h Hh] s k i a b /=. by case: ifP => Ha //; case: ifP => Hb. rewrite <- map_comp. do 2!(case: ifP => [/eqP <- /mapP[j Hj ->]| _] /=; first by move: Hj; rewrite select_children_spec => /andP[Hj _]; destruct h; rewrite // sym_tanner_rel). by rewrite has_map => /hasP[j] Hj /Hh. 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