proposition: Lemma comb_dprojs_not_in_partition d A (g : A -> {set 'I_n}) n0 t : [forall a, n0 \notin g a] -> (comb d (dprojs d g t) g) ``_ n0 = d ``_ n0.
proof: Proof. move=> /forallP H0. rewrite comb_out //. case: pickP => // m0. by rewrite (negbTE (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