proposition: Lemma measure_node (G : graph2) V E (con : @consistent _ _ G V E) v x y : connected [set: skeleton G] -> v \notin V -> measure (@point (subgraph_for con) x y) < measure G.
proof: Proof. move => /connectedTE conn_G Hv. case/connect_irredP : (conn_G v (val x)) => p _. have vx: v != val x. { apply: contraNN Hv => /eqP->. exact: valP. } case: (splitL p vx) => u [vu] _ {p vx}. move: vu. rewrite /=/sk_rel. case/andP=> _ /existsP[e He]. refine (@measure_subgraph _ _ _ _ _ _ e _). apply: contraNN Hv. move/con =>H. move: He. by rewrite !inE => /orP[/andP[/eqP<- _]|/andP[_ /eqP<-]]. 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)