proposition: Lemma fit_normq (x : G) q : fitq x (normq q) = fitq x q.
proof: Proof. by case: q => *; rewrite /fitq /= ?cats0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring quiz cfmap) fourcolor(cfquiz cfreducible)