proposition: Lemma forestI S : ~ (exists x y (p1 p2 : Path x y), [/\ irred p1, irred p2 & p1 != p2] /\ [/\ x \in S, y \in S, p1 \subset S & p2\subset S]) -> is_forest S.
proof: Proof. move=> H x y p1 p2 [Ip1 Sp1] [Ip2 Sp2]. case: (altP (p1 =P p2)) => // pN12. have [xS yS] : x \in S /\ y \in S. { by split; apply: (subsetP Sp1); rewrite ?path_begin ?path_end. } case: H. exists x; exists y; exists p1; exists p2. by repeat split. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)