proposition: Lemma measure_lens_rest (G : graph2) C : CK4F G -> lens G -> C \in @components G (@sinterval G input output) -> measure (induced2 (~: C)) < measure G.
proof: Proof. move=> G_CK4F G_lens. rewrite lens_sinterval //; last by case: G_CK4F. exact: measure_remove_component. 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)