proposition: Lemma measure_lens (G : graph2) C : CK4F G -> lens G -> edge_set G IO == set0 -> C \in components (@sinterval (skeleton G) input output) -> measure (component C) < measure G.
proof: Proof. set sI := sinterval _ _. case/and3P: (partition_components sI). set P := components _. move=> /eqP compU compI comp0 G_CK4F G_lens Eio0 C_comp. case: (lens_components G_CK4F G_lens Eio0 C_comp) => [D] D_comp DNC. have /set0Pn[x x_D] : D != set0 by apply: contraTneq D_comp =>->. move/trivIsetP: compI => /(_ D C D_comp C_comp DNC)/disjointFr/(_ x_D) xNC. have G_conn : connected [set: skeleton G] by case: G_CK4F. suff : x \notin input |: (output |: C) by exact: measure_node. have : x \in sI by rewrite -compU; apply/bigcupP; exists D. rewrite ![in ~~ _]inE xNC orbF. apply: contraTN =>/orP[]/eqP->; by rewrite (@sinterval_bounds 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)