proposition: Lemma fitqz_swap (y : G) qa1 qa2 qa3 q1 q2 q3 : fitqz y (quiz3 qa1 qa2 qa3 q1 q2 q3) = fitqz (face y) (Quiz (QaskR qa1 q1) (QaskR qa3 (QaskLR qa2 q3 q2))).
proof: Proof. rewrite /fitqz /= !eqseq_cons -!catA !fitq_cat !map_cons !eqseq_cons fitq_cat. rewrite /qstepR /qstepL !De2 -{1}[node (edge y)]nodeK !arity_face faceK. by rewrite -{1 2}[edge y]edgeK De2 Dn3 -{10 11}[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)