proposition: Lemma qzt_fit_store qz t : qzt_fit (store_qz qz t) -> (isQuizR qz /\ exists y : G, fitqz y qz) \/ qzt_fit t.
proof: Proof. case: qz => q1 []; auto; case: q1; auto => qa1 q1 qa2 q2 qz_t. set qz := Quiz _ _; pose fit_qzt := (exists y : G, fitqz y qz) \/ qzt_fit t. suffices: fit_qzt by case; [left | right]. have fit_q1LR qa1r q1l q1r: normq q1 = QaskLR qa1r q1l q1r -> qzt_fit (qzt_put qa1 qa2 qa1r q1l q2 q1r t) -> fit_qzt. - move=> Dq1 /qzt_fit_put[[y fit_y]|]; [left; exists y | by right]. by move: fit_y; rewrite -Dq1 /fitqz !eqseq_cons fitq_cat fit_normq -fitq_cat. have fit_q2LR qa2r q2l q2r: normq q2 = QaskLR qa2r q2l q2r -> qzt_fit (qzt_put qa1 qa2r qa2 q1 q2r q2l t) -> fit_qzt. - move=> Dq2 /qzt_fit_put[[y fit_y]|]; [left; exists (face y) | by right]. apply: etrans fit_y; rewrite fitqz_swap -Dq2 /fitqz !eqseq_cons !fitq_cat. by rewrite /= !eqseq_cons; congr [&& _, _, _ & _]; apply/esym/fit_normq. move: qz_t => /=. case Dq1: (normq q1); case Dq2: (normq q2); try case: ifP; by [right | eauto]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring quiz cfmap) fourcolor(cfquiz cfreducible)