proposition: Lemma comb_dprojs_V_not_in_partition d n0 t n1 : (forall m0, n1 \notin sgraph n0 m0) -> (comb_V d n0 (dprojs_V d n0 t)) ``_ n1 = d ``_ n1.
proof: Proof. move=> H0; rewrite /comb_V /dprojs_V comb_dprojs_not_in_partition //. apply/forallP => m0; by rewrite H0. 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