proposition: Lemma measure_remove_component (G : graph2) (C : {set G}) : CK4F G -> C \in @components G (~: IO) -> measure (induced2 (~: C)) < measure G.
proof: Proof. move=> [G_conn _] C_comp. case/and3P: (@partition_components G (~: IO)) => /eqP compU _ compN0. have /set0Pn[x x_C] : C != set0 by apply: contraTneq C_comp =>->. have {x_C} : x \notin ~: C by rewrite inE negbK. have : (input : G) \notin ~: IO by rewrite !inE negbK eqxx. have : (output : G) \notin ~: IO by rewrite !inE negbK eqxx. rewrite -compU. move/bigcupP/(_ (ex_intro2 _ _ C C_comp _))=> /negP oNC. move/bigcupP/(_ (ex_intro2 _ _ C C_comp _))=> /negP iNC. have {iNC oNC} [iNC oNC] : input \in ~: C /\ output \in ~: C by rewrite !inE. rewrite induced2_induced. exact: measure_node. Qed.
imports: Coq(RelationClasses Morphisms Setoid Lia) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries) GraphTheory(digraph sgraph minor checkpoint cp_minor) GraphTheory(setoid_bigop structures pttdom ptt) GraphTheory(mgraph mgraph2 skeleton bounded)