proposition: Lemma small_qarityP a : let qa := small_qarity a in bad_small_arity qa = (qa != a.+2 :> nat).
proof: Proof. by move: a; do 8!case=> //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring patch cfmap quiz)