proposition: Lemma qzt_fit_store_cf qz sym t : qzt_fit (store_cf_qz qz sym t) -> [/\ isQuizR qz & (exists y : G, fitqz y qz) \/ (exists y : mirror G, fitqz y qz)] \/ qzt_fit t.
proof: Proof. rewrite /store_cf_qz /=; case: sym; do!case/qzt_fit_store; try tauto. case=> qzR [y]; have {}qzR: isQuizR qz by case: (qz) qzR => q1 []; case: q1. by rewrite fitqz_flip //; left; split; last by right; exists (face y). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring quiz cfmap) fourcolor(cfquiz cfreducible)