proposition: Lemma card_nodes2 k p : p \in free_coports -> #|[set x in dest_port | x.1 == p & #|x.2| == k.+1]| = if p \in known_coports c then ([exists x in conodes c, (p \in x) && (#|x| == k.+1)] : nat) else 'C(#|port|.-1 - #|known_coports c|, k).
proof: Proof. move => Hp. have {}Hp: p \notin (graph_dom (conodes c)). move: Hp. by rewrite /free_coports !inE. case: ifPn => Hp'. - rewrite inE Hp' andbT negbK in Hp. case: existsP. + move => [x] /and3P[Hxc Hpx Hx]. apply (@eq_card1 _ (p,x)) => [] [p' x']. rewrite !inE /= xpair_eqE. case Hpp': (p' == p); last by rewrite andbF. rewrite (eqP Hpp') Hp' Hp /=. case Hxx': (x' == x). rewrite (eqP Hxx') Hpx Hx. by rewrite trivIset_in // part_p. case Hpx': (p \in x') => //=. case: trivIsetP => //= /(_ x' x). rewrite !inE eqxx Hxc /= orbT Hxx' => /(_ erefl erefl erefl). by rewrite (disjoint_I_false Hpx'). + move=> He. apply eq_card0 => [] [p' s]. rewrite 2!inE /=. apply/negbTE/negP. move/andP => [/and3P[Hpf Hps Hsc]] /andP [/eqP Hp'p Hsk]. subst p'. apply He; exists s. rewrite Hsk Hps. by rewrite (trivIset_I1 Hsc Hps). - clear Hp. transitivity ('C(#|port| - #|p |: known_coports c|, k)); first last. by rewrite cardsU1 Hp' subnDA subn1. rewrite -card_nodes dest_port_out //. apply card_in_imset => x y Hx Hy [] Hxy. apply/setP => z. move/setP/(_ z): Hxy. rewrite !inE. case: eqP => /= [-> _ | _ ->] //. rewrite !inE in Hx Hy. move/andP/proj2/disjoint_setI0/setP/(_ p): Hx. move/andP/proj2/disjoint_setI0/setP/(_ p): Hy. by rewrite !inE !eqxx !andbT /= => -> ->. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner