proposition: Lemma qzt_fit_put qa1 qa2 qa3 q1 q2 q3 t : qzt_fit (qzt_put qa1 qa2 qa3 q1 q2 q3 t) -> (exists y : G, fitqz y (quiz3 qa1 qa2 qa3 q1 q2 q3)) \/ qzt_fit t.
proof: Proof. rewrite /qzt_put /qzt_put3rot. case (8 < qa1); first by case/qzt_fit_put3; auto; left; exists (edge x2). case/qzt_fit_put3; first by left; exists (edge x2). case/qzt_fit_put3; first by rewrite fitqz_rot nodeK; left; exists (edge x1). case/qzt_fit_put3; auto. by rewrite 2!fitqz_rot -[x1]Dn3 !nodeK; left; exists (edge x3). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring quiz cfmap) fourcolor(cfquiz cfreducible)