proposition: Lemma sk_rel_mergeE (G : graph) (e : equiv_rel G) x y : @sk_rel _ _ (merge G e) x y <-> x != y /\ exists x0 y0 : skeleton G, [/\ \pi x0 = x, \pi y0 = y & x0 -- y0].
proof: Proof. rewrite /= /sk_rel. case: (boolP (x != y)) => //=; last by move => _; split => [|[]]. move => xy; split. - move => A. split => //. move: xy. pattern x, y. apply adjacentP => //. + move => {x y A} x y H xy. case: H => [|x0 [y0] [? ? /andP [E A]]]; first by rewrite eq_sym. exists y0; exists x0. by rewrite /edge_rel/=/sk_rel eq_sym adjacent_sym A E. + move => e0. exists (@endpoint _ _ G false e0). exists (@endpoint _ _ G true e0). split => // ; last apply/andP;split => //. * apply: contraNN xy => /eqP H. by rewrite eqmodE H. * apply/existsP; exists e0. by rewrite !inE !eqxx. - case => _ [x0] [y0] [Px Py /andP [Dxy0]]. case/existsP => [e0 E]. wlog E : x0 y0 x y Dxy0 Px Py {xy E} / e0 \in edges x0 y0. { move => W. case/setUP : E; first exact: W. rewrite adjacent_sym. apply: W => //. by rewrite eq_sym. } rewrite inE in E. case/andP : E => [E1 E2]. apply/existsP; exists e0. by rewrite !inE /= (eqP E1) (eqP E2) Px Py !eqxx. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient bij preliminaries) GraphTheory(digraph sgraph treewidth minor checkpoint) GraphTheory(setoid_bigop structures mgraph mgraph2)