proposition: Lemma is_forestPn (S : {set G}) : reflect (exists x y (p1 p2 : IPath x y), [/\ p1 \subset S, p2 \subset S & p1 != p2]) (~~ is_forestb S).
proof: Proof. rewrite negb_forall. apply: existsPP => x. rewrite negb_forall. apply: existsPP => y. rewrite -ltnNge. apply: (iffP card_gt1P) => /=. all: by move => [p1] [p2] [A B C]; exists p1; exists p2. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)