proposition: Lemma measure_card (G' G : graph2) : #|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)