fact: Definition rqs_proper (qs : rqseq) := let r0 := cpring G0 in let r := cpring G in let hr := map h r in [/\ rqs_fit qs r, {subset [predD r0 & [predU codom h & fband hr]] <= good_ring_arity}, simple (rqs_walk qs hr ++ r0) & fband (rqs_walk qs hr ++ r0) =i [predU [predC codom h] & fband hr]].
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring patch cfmap quiz)