proposition: Lemma measure_io (G' G : graph2) : (input == output :> G) -> (input != output :> G') -> #|edge G'| <= #|edge G| -> measure G' < measure G.
proof: Proof. rewrite /term_of_measure. do 2 case: (input == output) => //=; slia. 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)