proposition: Lemma qzt_fit_cfquiz cfs1 : qzt_fit (cfquiz_tree cfs1) -> exists2 i, i < size cfs1 & exists2 qz, (exists y : G, fitqz y qz) \/ (exists y : mirror G, fitqz y qz) & let r := cfring (nth cf000 cfs1 i) in embeddable r /\ (exists u, valid_quiz r u qz).
proof: Proof. rewrite /cfquiz_tree. have: qzt_fit qzt_empty = false. by rewrite /qzt_fit andbC; case: ax1 => //; case: ax2 => //; case ax3. elim: cfs1 qzt_empty => [|cf cfs1 IHcfs] qt0 /= => [-> // | fit'qt0]. have fit'nil: ~ qzt_fit QztNil by case/andP. set qt := store_cf_qz _ _ qt0. case Dqt: qt => // [t58 t9 t10 t11]; rewrite -{t58 t9 t10 t11}Dqt => fit_cfs1. case fit_qt: (qzt_fit qt); last by have [//| i] := IHcfs _ fit_qt; exists i.+1. case/qzt_fit_store_cf: fit_qt fit'qt0 => [[cfR fit_cf] _ | -> //]. exists 0 => //; exists (cfquiz cf) => //. by split; [apply: embeddable_cfquiz | apply: valid_cfquiz]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring quiz cfmap) fourcolor(cfquiz cfreducible)