proposition: Lemma rqs_fit_cons (rq : ring_question) qs x p : rqs_fit (rq :: qs) (x :: p) = [&& arity (h x) == rq + arity x, fitq (node (h x)) rq & rqs_fit qs p].
proof: Proof. by []. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring patch cfmap quiz)