fact: Definition comb d A (f : {ffun A -> 'rV[F]_n}) (g : A -> {set 'I_n}) := locked (\row_(j < n) (if [pick a | j \in g a] is Some a then (f a) ``_ j else d ``_ j)).
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