proposition: Lemma get_esti_subseq n0 l : subseq (map (pair (inr n0)) (@get_esti m n' n0 l)) l.
proof: Proof. elim: l => [|[i p] l IH] //. rewrite [get_esti _ _]/=. case: ifP => Hi. by rewrite /= (eqP Hi) eqxx. by eapply subseq_trans; [| apply subseq_cons]. 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