proposition: Lemma treeI S : connected 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_tree S.
proof: Proof. move => A B. split => //. exact: forestI. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)