proposition: Lemma measure_subgraph (G : graph2) V E (con : @consistent _ _ G V E) x y e : e \notin E -> measure (@point (subgraph_for con) x y) < measure G.
proof: Proof. move => He. apply: measure_card. rewrite card_sig. apply: proper_card. apply/properP. split; by [exact/subsetP| exists e]. 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)