proposition: Lemma rqs_fit_size qs p : rqs_fit qs p -> size qs = size p.
proof: Proof. by elim: qs p => [|rq qs IHrq] [|x p] //= /and3P[*]; congr _.+1; auto. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring patch cfmap quiz)