proposition: Lemma measure_igraph (G : graph2) : connected [set: skeleton G] -> (edge_set (@bag G IO input) != set0) || (edge_set (@bag G IO output) != set0) -> measure (@igraph _ _ G input output) < measure G.
proof: Proof. move=> G_conn A. suff [e] : exists e, e \notin @interval_edges _ _ G input output by exact: measure_subgraph. have [i_cp o_cp] : input \in @CP G IO /\ output \in @CP G IO by split; apply: CP_extensive; rewrite !inE eqxx. case/orP: A => /set0Pn[e He]; exists e; last rewrite interval_edges_sym. all: by rewrite (disjointFr (interval_bag_edges_disj G_conn _ _) He). 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)