proposition: Lemma conode_outside_ports i (j : {set port}) : i \notin known_coports c -> i \in j -> trivIset (j |: conodes c) -> j \subset ~: known_coports c.
proof: Proof. move=> Hi Hij Htriv. apply/subsetP => x Hx. rewrite inE. move: Hi; apply contra => Hxc. apply/bigcupP; exists j => //. by rewrite (trivIset_I1 Htriv Hx). Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner