proposition: Lemma fitqz_flip G x qz : plain_cubic G -> isQuizR qz -> @fitqz G x (flipqz qz) = @fitqz (mirror G) (face x) qz.
proof: Proof. case: qz => [] [] // qa0 q01 [] //= qa1 q10 [plainG cubicG] _. move Dh: (fun y : G => y : mirror G) => h. rewrite (congr1 (fun f => f (face x)) Dh); move: x. have [e2 n3] := (plain_eq plainG, cubic_eq cubicG). have nFh: {mono h : x / arity x} by move=> x; rewrite -Dh arity_mirror. have hL: {morph h : x / qstepR x >-> qstepL x}. move=> x; rewrite -Dh /= (f_finv nodeI) -{2}[x]e2 -[edge x]n3 nodeK. by rewrite (finv_f nodeI). have hR: {morph h : x / qstepL x >-> qstepR x}. by move=> x; rewrite hL -Dh /qstepL /qstepR /= (finv_f nodeI). have{Dh} hE x: edge (h (face x)) = h (face (edge x)). by rewrite -Dh /= -{1}[x]e2 edgeK. have nFen G1 x: arity (@edge G1 (node x)) = arity x. by rewrite -arity_face nodeK. move: (mirror G) => G1 in h nFh hL hR hE *. have fit_flip q x: fitq x (flipq q) = fitq (h x) q. rewrite /fitq; elim: q x => //= *; rewrite -?hL -?hR ?nFen nFh //; rewrite !eqseq_cons ?fitq_cat /fitq; try congr (_ && _); try by []. by rewrite /fitq andbC; congr (_ && _). move=> x; rewrite /fitqz /= !eqseq_cons !fitq_cat /= !eqseq_cons hE !nFh. rewrite !arity_face -!hR !(andbCA (fitq _ _)); congr [&& _, _ & _]. rewrite -fit_flip fit_flip andbC; congr (_ && _); congr (_ == map _ _). by rewrite /qstepR /qstepL e2 faceK. by rewrite /qstepL edgeK. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry coloring)