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