proposition: Lemma qzt_get1_truncate qa t : let t' := qzt_get1 qa (qzt_truncate t) in qzt_proper t' -> t' = qzt_get1 qa t.
proof: Proof. by case: qa t => [] // [] // []. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring quiz cfmap) fourcolor(cfquiz cfreducible)