proposition: Lemma connected_igraph (G : graph2) (x y: G) : connected [set: skeleton G] -> connected [set: skeleton (igraph x y)].
proof: Proof. move=> conn_G. apply: connected_skeleton; rewrite imset_valT memKset. + exact: connected_interval. + move => e E1 E2. rewrite 4!inE E1 andbT negb_or. apply/andP;split. * apply: contraNN E2 => /andP [/eqP -> /eqP ->]; by rewrite eqxx. * apply: contraNN E2 => /andP [/eqP -> /eqP ->]; by rewrite eqxx. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient bij preliminaries) GraphTheory(digraph sgraph treewidth minor checkpoint) GraphTheory(setoid_bigop structures mgraph mgraph2)