proposition: Lemma connected_add_node (G : sgraph) (U A : {set G}) : connected A -> @connected (add_node G U) (Some @: A).
proof: Proof. move => H x y /imsetP [x0 Hx0 ->] /imsetP [y0 Hy0 ->]. have/connect_irredRP := H _ _ Hx0 Hy0. case: (x0 =P y0) => [-> _|_ /(_ isT) [p _ Hp]]; first exact: connect0. case: (add_node_lift_Path U p) => q E. apply: (connectRI q) => ?; rewrite mem_path E. case/mapP => z Hz ->. rewrite imset_f //. exact: (subsetP Hp). Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph) GraphTheory(set_tac)