proposition: Lemma valid_cfquiz : exists u, valid_quiz (cfring cf) u cfquiz.
proof: Proof. case: cfquizP => _ [u [qz_ok qz_u Uqz Eqz]]; exists u; split; auto => v. by rewrite Eqz !inE -fband_rev. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring patch cfmap quiz)