proposition: Lemma rqs_walk_cons (rq : ring_question) qs u p : rqs_walk (rq :: qs) (u :: p) = nseq (isk rq) u ++ walkq (node u) rq ++ rqs_walk 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)