proposition: Lemma comb_V2_freeon d m0 n0 (m0n0 : n0 \in 'V m0) t' t (Ht : freeon ('V m0 :\ n0) d t') : comb_V2 H d m0 n0 (dprojs_V2 H d m0 n0 t) = t -> freeon (`V(m0, n0) :\ n0) t' t.
proof: Proof. move=> <-. apply: (freeon_trans m0n0 Ht). apply/forallP => /= n1. rewrite in_setD1 negb_and negbK. apply/implyP => /orP[/eqP ->{n1}|]. by rewrite comb_dprojs_V2_Vnext // (freeon_notin Ht) // !inE eqxx. move=> Hn1. by rewrite comb_dprojs_V2_not_in_subgraph. 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