proposition: Lemma card_nodes k (P : {set port}) : #| [node x $ k | [disjoint x & P] ] | = 'C(#|port| - #|P|, k).
proof: Proof. set A := (X in #|pred_of_set X| = _). have -> : A = [set x : {set _} | x \subset ~: P & #|x| == k]. apply/setP => ?; by rewrite !inE subsets_disjoint setCK andbC. by rewrite cards_draws cardsCp. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner