proposition: Lemma join_is_forest : is_forest [set: sjoin T1 T2].
proof: Proof. Proof with try solve [exact: inl_inj|exact: inr_inj |exact: sub_inl|exact: sub_inr]. move => [a|a] [b|b] p q [Ip _] [Iq _]. - case: (lift_Path (p' := p)) => //... case: (lift_Path (p' := q)) => //... move => p' Np I q' Nq I'. have E : p' = q'. { apply: forestP; by rewrite ?I ?I'. } apply/eqP. by rewrite -nodes_eqE -Nq -E Np. - move: (Path_connect p). by rewrite join_disc. - move: (Path_connect p). by rewrite sconnect_sym join_disc. - case: (lift_Path (p' := p)) => //... case: (lift_Path (p' := q)) => //... move => p' Np I q' Nq I'. have E : p' = q'. { apply: forestP; by rewrite ?I ?I'. } apply/eqP. by rewrite -nodes_eqE -Nq -E Np. Qed.
imports: Coq(RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) GraphTheory(connectivity set_tac)