proposition: Lemma trivIset_port_out (x : {set port}) : [disjoint x & p |: known_coports c] -> trivIset (p |: x |: conodes c).
proof: Proof. move=> Hxp. apply trivIset_out; first by apply part_p. rewrite disjointsU1 Hp. move: Hxp. by rewrite disjoint_sym disjointsU1 disjoint_sym => /andP [_ ->]. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner