proposition: Lemma comb_dprojs_V2_Vnext d t n0 m0 (m0n0 : n0 \in 'V m0) : (comb_V2 H d m0 n0 (dprojs_V2 H d m0 n0 t)) ``_ n0 = d ``_ n0.
proof: Proof. rewrite /comb_V2 comb_out //. case: pickP => [ n2 | // ]. rewrite inE => /andP[Hn2 /existsP[m1 /andP[Hm1]]]. move/(notin_Vgraph Hacyclic) : m0n0. by move/(_ _ _ Hn2 Hm1) => /negbTE => ->. 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