proposition: Lemma fitqa_popqa r qa : fitqa r qa -> forall n, r n && (popqa r 9 || ~~ popqa r n) -> n = qa.
proof: Proof. by case: r qa => -[] // _; do 9!case=> //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry part quiz quiztree)