proposition: Lemma comb_dprojs_V2 d m0 n0 (m0n0 : n0 \in 'V m0) d' t (d'td : dproj d' ('V m0 :\ n0) t = d) (d't : freeon (`V(m0, n0) :\ n0) d' t) : comb_V2 H d m0 n0 (dprojs_V2 H d m0 n0 t) == t.
proof: Proof. apply/eqP/rowP => n1. case/boolP : (n1 == n0) => [/eqP ?|n1n0]. subst n1. rewrite comb_dprojs_V2_Vnext // -d'td dproj_out ?in_setD1 ?eqxx //. move/rowP : d'td => /(_ n0). by rewrite (freeon_notin d't) // in_setD1 eqxx. case/boolP : [exists n2, n1 \in ssgraph H m0 n0 n2] => [/existsP[n2 Hn2]|]. rewrite comb_dprojs_V2_in_partition //; by exists n2. rewrite negb_exists => H0. rewrite comb_out; last first. case: pickP => // => x. by move/forallP : H0 => /(_ x) /negbTE ->. rewrite -d'td. case/boolP : (n1 \in 'V m0 :\ n0) => K. by rewrite dproj_in. rewrite dproj_out //. move/forallP: d't => /(_ n1). rewrite in_setD1 n1n0 /=. have -> : n1 \notin `V(m0, n0). apply/negP => n1m0n0. rewrite in_setD1 negb_and negbK (negbTE n1n0) orFb in K. case: (Vgraph_decompose m0n0 n1m0n0 n1n0 K) => n2 [] Hn2 [m1 [H0' H1']]. move/forallP in H0. move: (H0 n2) => /=; rewrite /ssgraph Hn2 /= inE. by rewrite negb_exists => /forallP/(_ m1); rewrite H0' /= H1'. by rewrite implyTb => /eqP. 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