proposition: Lemma measure_redirect (G : graph2) C : CK4F G -> input == output :> G -> C \in @components G [set~ input] -> measure (redirect C) < measure G.
proof: Proof. move => CK4F_G Eio HC. have D := @partition_components G [set~ input]. have Csub: C \subset [set~ input]. { rewrite -(cover_partition D). apply/subsetP => z Hz. exact: mem_cover HC _. } rewrite /redirect. case: pickP => [x /andP [Hx1 Hx2]|]. - apply: measure_io => //=. + rewrite -val_eqE /=. apply: contraTN Hx1 => /eqP<-. apply: contraTN Csub => A. apply/subsetPn. exists input => //. by rewrite setC11. + rewrite card_sig. exact: max_card. - move => _. apply: measure_card => /=. rewrite card_void. have/set0Pn [x Hx] : C != set0. { case/and3P : D => _ _. by apply: contraNN => /eqP <-. } have: x != input. move/(subsetP Csub) in Hx. by rewrite !inE in Hx. apply: has_edge. by apply CK4F_G. 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)