proposition: Lemma link_is_forest : is_forest [set: link].
proof: Proof. apply: unique_forestT => x y p q Ip Iq. case: (boolP (None \in p)) => Np. - have Nq := link_has_None Ip Iq Np. case/(isplitP Ip) def_p : _ / Np => [p1 p2 Ip1 Ip2 _]. case/(isplitP Iq) def_q : _ / Nq => [q1 q2 Iq1 Iq2 _]. congr pcat. + apply: prev_inj. apply: link_unique_None; by rewrite irred_rev. + exact: link_unique_None. - suff Nq : None \notin q by apply: link_unique_lift. apply: contraNN Np. exact: link_has_None. Qed.
imports: Coq(RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) GraphTheory(connectivity set_tac)