proposition: Lemma adjn_merge1 (d1 d2 : D) : ~~ @cnode[D] dx dy -> ~~ @adjn[D] dx dy -> @cnode[D] d1 dy -> @adjn[D'] d1 d2 = @adjn[D] d2 dx || @adjn[D] d2 dy.
proof: Proof. move=> n_dxy nAdydx d1y. 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/idP/idP. - case/exists_inP => z; rewrite !inE; set z' := edge z => C1. have {d1 d1y C1} Cz : @cnode[D'] dy z. { apply: connect_trans C1. rewrite cnodeC. exact: switch_subrel d1y. } move: (Cz); rewrite cnode_merge // [_ dy dx]cnodeC (negbTE n_dxy) connect0 /=. rewrite cnode_merge // [@cnode[D] z' dx]rwF 1?[@cnode[D] z' dy]rwF ?andbF ?orbF. + case/orP => H1 H2; apply/orP; [right|left]; apply/exists_inP; exists (edge z) => //. by rewrite plain_eq. by rewrite plain_eq // inE cnodeC. + apply: contraNN llD' => X; apply/existsP; exists z; rewrite cnodeC. apply: connect_trans Cz. exact: subDD'. + apply: contraNN llD' => X; apply/existsP; exists z; rewrite cnodeC. apply: connect_trans Cz. apply: connect_trans. exact: subDD' X. done. - case/orP; case/exists_inP => z; rewrite !inE => d2_z d_ez. + apply/exists_inP; exists (edge z); rewrite inE. * apply: connect_trans (subDD' _ _ d_ez). apply: connect_trans (subDD' _ _ d1y) _. by rewrite cnodeC. * rewrite plain_eq //. exact: subDD'. + apply/exists_inP; exists (edge z); rewrite inE. * apply: connect_trans (subDD' _ _ d_ez). exact: subDD'. * rewrite plain_eq //. exact: subDD'. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)