proposition: Lemma skip_skip1 (G : hypermap) (p : pred G) (z : G) (f : G -> G) (injf : injective f) (x : G) (xDz : x != z) : let G' := WalkupF z in let p' := fun x : G' => p (val x) in ~~ p z -> p x -> skip p f x = sval (skip p' (@walkup.skip (permF G) z f injf) (Sub x xDz)).
proof: Proof. move => G' p' npz px. symmetry. case: skipP => //. exact: inj_skip. move => n _ N1 N2. have [y Y1 Y2] : exists2 y, p y & fconnect f (f x) y. { exists x => //. by rewrite -same_fconnect1. } elim: n x xDz {px} Y2 N1 N2 => [|n IHn] x xDz Y2 N1 N2. - rewrite /=. case: (altP (f x =P z)) => [EQ|NEQ]. + rewrite (skip_first y) // EQ // skip1 //. move: N1. by rewrite /walkup.skip unfold_in /= EQ eqxx. + rewrite skip1 //. move: N1. by rewrite /walkup.skip unfold_in /= (negbTE NEQ). - rewrite iterSr. set wfx := walkup.skip _ _. have npfx : ~~ p' wfx. apply/negP => pfx. move: (N2 0) => /=. by case/(_ _)/Wrap. pose fx := (if f x == z then f z else f x). rewrite [n.+1]lock /wfx {2}/walkup.skip. move: (skip_subproof _ _) => /= fxDz. rewrite -lock IHn. + rewrite /fx. case: (altP (f x =P z)) => [EQ|NEQ]; last first. * rewrite [RHS](skip_first y) //. apply: contraNN npfx. by rewrite /wfx/walkup.skip/p'/= (negbTE NEQ). * rewrite [RHS](skip_first y) // ?EQ //. rewrite [RHS](skip_first y) //. by rewrite -EQ -same_fconnect1. apply: contraNN npfx. by rewrite /wfx/walkup.skip/p'/= EQ eqxx. + rewrite /fx. case: (altP (f x =P z)) => [EQ|NEQ]; last first. * by rewrite -same_fconnect1. * by rewrite -EQ -2!(same_fconnect1 injf). + rewrite [Sub fx fxDz](_ : _ = wfx) /wfx -?iterSr //. exact: val_inj. + move => m. rewrite [Sub fx fxDz](_ : _ = wfx) /wfx -?iterSr. apply: N2. exact: val_inj. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij) fourcolor(hypermap geometry cfmap jordan color coloring combinatorial4ct) fourcolor(walkup)