proposition: Lemma comb_dprojs_V2_in_partition d t m0 n0 n1 : (exists n2, n1 \in ssgraph H m0 n0 n2) -> (comb_V2 H d m0 n0 (dprojs_V2 H d m0 n0 t)) ``_ n1 = t ``_ n1.
proof: Proof. case=> n2 Hn2. have [n2' Hn2'] : exists n2', [pick a | n1 \in ssgraph H m0 n0 a] = Some n2'. case: pickP Hn2 => [x Hx _ | /(_ n2) -> //]; by exists x. rewrite (@comb_in _ _ _ _ _ _ _ n2') //. rewrite dprojs_in; first by []. case: pickP Hn2'. by move=> x hx [<-]. move=> _ ?. by exfalso. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg zmodp matrix) Reals mathcomp(Rstruct) ssr_ext ssralg_ext ssrR Reals_ext f2 summary subgraph_partition tanner tanner_partition fdist channel checksum