proposition: Lemma get_esti_nil n0 k (t : tn_tree' k) : inr n0 \notin labels t -> size (get_esti n0 (estimation t)) = 0%N.
proof: Proof. move: k t; refine (children_ind _) => k [id0 tag0 ch0 up0 down0] /= IH. rewrite in_cons => /norP [Hid0 Hfl]. suff : size (get_esti n0 (flatten [seq estimation i | i <- ch0])) = 0%N. destruct tag0; first by []. by rewrite /= (eq_sym id0) (negbTE Hid0). rewrite get_esti_flatten size_flatten sumnE big_seq/= big1// => i. rewrite /shape -!map_comp => /mapP[x Hx] -> /=. apply IH => //. apply/negP => Hlx. apply/negP: Hfl. rewrite negbK. apply/flattenP; exists (labels x); last by []. exact: (map_f labels). 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