proposition: Lemma mypath_ok_rec h a p : (size p) < h -> path myrel a p -> (a :: p \in mypath h).
proof: Proof. elim: h a p => [//|h IHh] a p Hp Hun. suff : a :: p \in flatten [seq [seq i :: l | l <- [::] :: mypath h & path myrel i l] | i <- enum_id] by []. apply /flattenP. exists [seq a :: l | l <- [::] :: mypath h & path myrel a l]. apply /mapP. exists a => //; by rewrite enum_id_ok. destruct p. by rewrite in_cons eqxx. apply /mapP. exists (s :: p) => //. rewrite mem_filter Hun in_cons IHh ?orbT //. simpl in Hun. by move /andP/proj2: Hun => ->. 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