proposition: Lemma path_in_connected (G:sgraph) (T : {set G}) x y : connected T -> x \in T -> y \in T -> exists2 p : Path x y, irred p & p \subset T.
proof: Proof. move => C Hx Hy. case: (altP (x =P y)) => [?|D]. - subst y. exists (idp x); rewrite ?irred_idp //. apply/subsetP => A. by rewrite mem_idp => /eqP->. - case/connect_irredRP : (C _ _ Hx Hy) => // p Ip Sp. by exists p. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)