proposition: Lemma comb_dprojs_V2_not_in_subgraph d t n0 m0 (m0n0 : n0 \in 'V m0) n1 : n1 \notin `V(m0, n0) -> (comb_V2 H d m0 n0 (dprojs_V2 H d m0 n0 t)) ``_ n1 = d ``_ n1.
proof: Proof. move=> Hn1. rewrite /comb_V2 comb_out //. case: pickP => [ n2 | // ]. rewrite inE => /andP[Hn2 H0]. suff : n1 \in `V(m0, n0) by rewrite (negbTE Hn1). case/existsP : H0 => [m1 /andP[H0 H1]]. by apply: (@Vgraph_inclusion _ _ _ Hacyclic n2 m0 n0 m1). 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