proposition: Lemma comb_out d A (f : {ffun A -> 'rV[F]_n}) (g : A -> {set 'I_n}) n1 : [pick a | n1 \in g a] = None-> (comb d f g) ``_ n1 = d ``_ n1.
proof: Proof. move=> Hn1; rewrite /comb; unlock => /=; by rewrite mxE Hn1. 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