proposition: Lemma fitqz_rot (y : G) qa1 qa2 qa3 q1 q2 q3 : fitqz y (quiz3 qa1 qa2 qa3 q1 q2 q3) = fitqz (edge (face y)) (quiz3 qa3 qa1 qa2 q3 q1 q2).
proof: Proof. rewrite /fitqz /= !eqseq_cons -!catA !fitq_cat !map_cons !eqseq_cons. rewrite /qstepL /qstepR !De2 faceK -{1}[node (edge y)]nodeK !arity_face. by rewrite -{1 2}[edge y]edgeK De2 Dn3 -{8 9}[y]De2 edgeK; do !bool_congr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring quiz cfmap) fourcolor(cfquiz cfreducible)