fact: Definition cfquiz_Y rq1 rq2 rqs' : rqseq := let: RingQuestion _ _ q1 := rq1 in let: RingQuestion k2 a2 q2 := rq2 in if k2 then let qa2 := small_qarity a2 in if bad_small_arity qa2 then [::] else rqs' match q1, q2 with | Qask0, Qask0 => Qask1 qa2 | Qask0, _ => QaskL qa2 q2 | _, Qask0 => QaskR qa2 q1 | _, _ => QaskLR qa2 q2 q1 end else if bad_ring_arity a2 then [::] else match q1, q2 with | Qask0, Qask0 => rqs' Qask0 | QaskR qa1 q1r, Qask0 => rqs' (QaskRR qa1 q1r) | Qask0, QaskL qa1 q1l => rqs' (QaskLL qa1 q1l) | _, _ => [::] end.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring patch cfmap quiz)