proposition: Lemma adjn_merge2 (d1 d2 : D) : ~~ @cnode[D] dx dy -> ~~ @adjn[D] dx dy -> ~~ @cnode[D] d1 dx -> ~~ @cnode[D] d1 dy -> ~~ @cnode[D] d2 dx -> ~~ @cnode[D] d2 dy -> @adjn[D'] d1 d2 = @adjn[D] d1 d2.
proof: Proof. move=> n_dxy nAdydx d1x d1y d2x d2y. have llD' : loopless D' by apply: merge_loopless. have dxdy : @cnode[D'] dx dy by rewrite fconnect_switched => //; exact: (@nodeI D). have subDD' : subrel @cnode[D] @cnode[D'] by apply: switch_subrel. apply/exists_inP/exists_inP => -[z]; rewrite !inE. - rewrite fconnect_switchE //; last exact: (@nodeI D). rewrite (negbTE d1x) (negbTE d1y) // fconnect_switchE //; last exact: (@nodeI D). rewrite (negbTE d2x) (negbTE d2y) /= !orbF. by exists z. - move => d1z d2ez. exists z; apply: switch_subrel => //; exact: (@nodeI D). Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)