proposition: Lemma connected_start (pn : {set port}) : partial_connected (start_graph pn).
proof: Proof. move=> x y. rewrite /known_port /known_coports /ports /= big_set1 big_set0. case: x => [] x; case: y => [] y /=; try by rewrite inE. move => Hx Hy. case Hxy: (x == y). exists [::] => /=. exists false, false. by rewrite (eqP Hxy). exists [:: (inl y, true)] => /=. exists false, true. rewrite eqxx /= !andbT. apply/existsP; exists pn. by rewrite inE eqxx Hxy Hx Hy. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner