proposition: Lemma qzt_getr_fit r qt1 : qzt_proper (qzt_getr r qt1) -> let qa := topqa r in [/\ fitqa r qa, qzt_get1 qa qt1 = qzt_getr r qt1 & qzt_proper qt1].
proof: Proof. by case: qt1 => // qt5 qt6 qt7 qt8; case: r. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry part quiz quiztree)