proposition: Lemma dest_port_out : [set x in dest_port | x.1 == p & #|x.2| == k.+1] = [set (p, p |: x) | x in [node x $ k | [disjoint x & p |: known_coports c] ] ].
proof: Proof. apply/setP => [] [p' s]. rewrite !inE /=. symmetry. apply/imsetP. case: ifP. - move/andP=> [/and3P[Hpf Hps Hsc]] /andP [/eqP Hp'p Hsk]. subst p'. exists (s :\ p). rewrite (cardsD1 p) Hps add1n eqSS in Hsk. rewrite inE Hsk disjoints_subset. apply/subsetP => x. rewrite !inE negb_or -in_setC. case: (x == p) => //=. apply /subsetP: x. rewrite -disjoints_subset. by apply (trivIset_disjoint Hps). f_equal. apply/setP => x. rewrite !inE. by case: eqP => //= ->. - move/negP => Hneg [x Hx [Hp'p Hs]]. subst p' s. rewrite inE in Hx. move/andP: Hx => [Hxk Hxp]. apply: Hneg. rewrite eqxx negb_and Hp orbT !inE eqxx trivIset_port_out //=. rewrite cardsU1. case Hpx: (p \in x). + by rewrite (disjoint_I_false Hpx) // !inE eqxx in Hxp. + by rewrite add1n /= eqSS Hxk. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner