proposition: Lemma connected_induced (G : graph) (V : {set skeleton G}) : connected V -> connected [set: skeleton (induced V)].
proof: Proof. move => conV. apply: connectedTI => u v. move: (conV (val u) (val v) (valP u) (valP v)). case/upathPR => p /upathW. elim: p u => [?|a p IH u]. - move/pathp_nil/val_inj ->. exact: connect0. - rewrite pathp_cons /= -!andbA => /and5P [A B C D E]. apply: (connect_trans (y := Sub a B)); last exact: IH. apply: connect1. move: C. rewrite /edge_rel/=/sk_rel -val_eqE. by rewrite adjacent_induced. 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)