proposition: Lemma componentless_one (G : graph2) : input == output :> G -> edge_set G IO == set0 -> @components G [set~ input] == set0 -> G ≃2 1.
proof: Proof. move => Eio E com0. have A (x : G) : x = input. { set C := pblock (@components G [set~ input]) x. apply: contraTeq com0 => Hx. apply/set0Pn. exists C. apply: pblock_mem. by rewrite (cover_partition (partition_components _)) !inE. } apply: iso_one => // [x|e]; first by rewrite !inE [x]A eqxx. move/eqP/setP/(_ e) : E. by rewrite !inE [source e]A [target e]A !eqxx. 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)