proposition: Lemma qzt_fit_put3 qa1 qa2 qa3 q1 q2 q3 t : qzt_fit (qzt_put3 qa1 qa2 qa3 q1 q2 q3 t) -> fitqz (edge x2) (quiz3 qa1 qa2 qa3 q1 q2 q3) \/ qzt_fit t.
proof: Proof. case/andP=> Eax; rewrite /qzt_fit Eax /fitqz /= !eqseq_cons -arity_face nodeK. rewrite /qstepR De2 /qstepL Dn3 -!catA /= 2!fitq_cat map_cons eqseq_cons. have{Eax} [/eqP <- /eqP <- /eqP <-] := and3P Eax. rewrite /qzt_get3 /qzt_get2 /qzt_put3; set qr := QztLeaf q1 q2 q3. have [[<- <-]|<-] := qgp1 ax1 qa1 (qzt_put1 qa2 (qzt_put1 qa3 qr)) t; auto. have [[<- <-]|<-] := qgp1 ax2 qa2 (qzt_put1 qa3 qr) (qzt_get1 ax1 t); auto. have [[<- <-]|<-] := qgp1 ax3 qa3 qr (qzt_get1 ax2 (qzt_get1 ax1 t)); auto. by rewrite !eqxx !andTb /= [rhc in _ && rhc]andbC => /orP[]; auto. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring quiz cfmap) fourcolor(cfquiz cfreducible)