proposition: Lemma componentless_top (G : graph2) : input != output :> G -> @components G (~: IO) == set0 -> point (@remove_edges _ _ G (edge_set IO)) input output ≃2 top.
proof: Proof. move => Dio com0. have A (x: G) : x \in IO. { set C := pblock (@components G (~: IO)) x. apply: contraTT com0 => Hx. apply/set0Pn. exists C. apply: pblock_mem. by rewrite (cover_partition (partition_components _)) inE. } apply: iso_top => //. move => [e He]. rewrite inE negb_and in He. case/orP: He; by rewrite A. Qed.
imports: Coq(RelationClasses Morphisms Setoid) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries) GraphTheory(bij set_tac digraph sgraph minor checkpoint) GraphTheory(setoid_bigop structures pttdom mgraph mgraph2) GraphTheory(skeleton bounded equiv extraction_def)