proposition: Lemma measure_split_cpL : measure (igraph input z) < measure G.
proof: Proof. apply: (measure_node (v := output)); first apply CK4F_G. have Ho: output \in @interval G z output. exact: intervalR. apply: contraNN Zo => C. by rewrite eq_sym -in_set1 -(intervalI_cp Hz') inE C. 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)