proposition: Lemma node_of_hemi_comp_graph ep (en : {set port}) h : ep \in en -> en \in (part h) -> \bigcup_(en in h | ep \in en) en = en.
proof: Proof. move=> Hep Hen. rewrite (big_pred1 en) //= => en'. rewrite pred1E. case/boolP: (en == en') => Henn'. by rewrite -(eqP Henn') Hep Hen. case Hen': (en' \in h) => //=. apply/negP => Hep'. move/trivIsetP/(_ en en' Hen Hen' Henn'): (part_p h). by rewrite (disjoint_I_false Hep). Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner