proposition: Lemma connected_component_set (G : graph2) C : CK4F G -> lens G -> C \in components (@sinterval (skeleton G) input output) -> @connected G (input |: (output |: C)).
proof: Proof. set sI := sinterval _ _. move=> [G_conn G_K4F] G_lens C_comp. case: (sinterval_components C_comp) => -[u] u_C iu [v] v_C ov. apply: connectedU_edge iu _ _; rewrite 3?inE ?eqxx ?u_C //; first exact: connected1. apply: connectedU_edge ov _ _; rewrite 1?inE ?eqxx ?v_C //; first exact: connected1. exact: connected_in_components C_comp. 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)