proposition: Lemma comb_dprojs_V d i t : t ``_ i = d ``_ i -> comb_V d i (dprojs_V d i t) = t.
proof: Proof. move=> H0. rewrite /comb_V /dprojs_V comb_dprojs // => n1. case/boolP: (i == n1) => [/eqP <-|in1]; [by left | right]. move: (cover_Vgraph_part_vnode Hconnected i) => Hcover. have : n1 \in cover (Vgraph_part_vnode H i) :\ i by rewrite Hcover !inE eq_sym in1. rewrite in_setD1 eq_sym in1 /=. case/bigcupP => /= s /imsetP[m1 Hm1 ->{s} Hn1]; by exists 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