proposition: Lemma zdart_stepLt zp : zpfit_top zp -> zpvalid zp -> zpfit (qstepL (zdart zp)) (zstepLt zp).
proof: Proof. case: zp => zi pl pr zp_top /zdart_stepL; case: zi zp_top => // /eqP/Dfn->. by case: pl => // -[] // h pl _ _ /=; rewrite /qstepL !faceK nodeK Dnf. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry part quiz quiztree)