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