proposition: Lemma card_nodes3 (k : 'I_U) : k <> 0 -> (forall j : {set port}, i \in j -> trivIset (j |: conodes c) -> (#|j| < U)%nat) -> #| [node x $ k | (i \in x) && trivIset (x |: conodes c)] | = 'C(#|port|.-1 - #|known_coports c|, k.-1).
proof: Proof. move=> Hk Hcj. move: (@card_nodes2 k.-1 i). rewrite !inE. case: ifP => Hi'. by move: Hi; rewrite Hi'. rewrite andbF /= => /(_ erefl) <-. rewrite -(@card_imset _ _ (fun x : {set port} => (i, x))); last first. by move=> a b []. do !f_equal. apply/setP => [] [j s]. rewrite !inE /=. case Hij: (j == i) => /=. rewrite (eqP Hij) Hi' andbF /=. have <-: k = k.-1.+1 :> nat. rewrite prednK // lt0n. by move/eqP: Hk. case His: (_ && _ && _). by rewrite imset_f // inE andbC. apply/imsetP => [] [s' Hs' [Hss']]. by rewrite -Hss' !inE -topredE /= andbC His in Hs'. rewrite andbF. apply/imsetP => [] [s' Hs' [Hji]]. by rewrite Hji eqxx in Hij. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner