proposition: Lemma measure_remove_edges (G : graph2) (E : {set edge G}) (i o : G) : E != set0 -> measure (point (remove_edges E) i o) < measure G.
proof: Proof. case/set0Pn => e inIO. apply: measure_card => /=. rewrite card_sig. apply: (card_ltnT (x := e)). by rewrite /= negbK. 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)