proposition: Lemma qzt_get_put1 qa qa' qr t : qa = qa' /\ qr (qzt_get1 qa t) = qzt_get1 qa (qzt_put1 qa' qr t) \/ qzt_get1 qa t = qzt_get1 qa (qzt_put1 qa' qr t).
proof: Proof. by elim: t; auto; case qa'; auto; case qa; 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)