proposition: Lemma skel_union_join (G1 G2 : graph) : @sk_rel _ _ (union G1 G2) =2 @join_rel G1 G2.
proof: Proof. move => [x|x] [y|y] /=. - rewrite /edge_rel/=/sk_rel sum_eqE. case: (boolP (x == y)) => //= E. apply/existsP/existsP. + move => [[e|e]]; rewrite !inE //= !sum_eqE. by exists e; rewrite !inE. + move => [e] H. exists (inl e). by rewrite !inE /= !sum_eqE in H *. - apply: contraTF isT => /existsP [[e|e]]; by rewrite !inE //= andbC. - apply: contraTF isT => /existsP [[e|e]]; by rewrite !inE //= andbC. - rewrite /edge_rel/=/sk_rel sum_eqE. case: (boolP (x == y)) => //= E. apply/existsP/existsP. + move => [[e|e]]; rewrite !inE //= !sum_eqE. by exists e; rewrite !inE. + move => [e] H. exists (inr e). by rewrite !inE /= !sum_eqE in H *. Qed.
imports: Coq(RelationClasses Setoid) mathcomp(all_ssreflect) GraphTheory(edone set_tac finite_quotient preliminaries) GraphTheory(digraph sgraph treewidth minor equiv setoid_bigop) GraphTheory(structures mgraph pttdom ptt mgraph2 skeleton)