proposition: Lemma forest3 : is_forest [set: G] -> 3 <= #|G| -> exists x y : G, x != y /\ ~~ x -- y.
proof: Proof. move => /is_forestP forest_G card_G. setoid_rewrite (rwP andP). do ! setoid_rewrite (rwP existsP). apply: contraTT forest_G => P. have {P} comp_G : forall x y : G, x != y -> x -- y. { move => x y xDy. move/existsPn : P => /(_ x)/exists_inPn/(_ y xDy). by rewrite negbK. } case/card_gt2P : card_G => x [y] [z] [_ [D1 D2 D3]]. rewrite eq_sym in D1. apply/is_forestPn; exists y; exists x. pose p1 := Build_IPath (irred_edge (comp_G y x D1)). have Ip2 : irred (pcat (edgep (comp_G y z D2)) (edgep (comp_G z x D3))). { by rewrite irred_edgeL irred_edge andbT /= mem_edgep negb_or D1 D2. } pose p2 := Build_IPath Ip2. exists p1; exists p2. split => //. have: z \in p2 by rewrite !inE. apply: contraTneq => <-. by rewrite mem_edgep negb_or D3 eq_sym D2. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)