proposition: Lemma zdart_stepL zp : zpvalid zp -> zpfit (qstepL (zdart zp)) (zstepL zp).
proof: Proof. rewrite /zstepL /qstepL; case: zp => zi pl pr. case Dzi: zi => // [] zp_ok zp_proper; rewrite ?zdart_shiftr ?zdart_shiftl //= /zmove /= ?Dn3 //; do [by rewrite ?Dnf ?De2 // ?Dn2 ?De2 ?nodeK | move/zvalid_fit: zp_ok]. - rewrite fitp_catrev; move: zp_proper; rewrite zproper_shiftr -/(zorg pl). by case: pr => [|[] h|h f1|h f1 f2|h f1 f2 f3] //= pr _ /and3P[_ Ds _]; rewrite Dnf [in LHS](Dfn Ds) ?faceK !Dn2 !De2 -!Dnf Dn2 !Dnf. by case: pl zp_proper => [|[] h|h f1|h f1 f2|h f1 f2 f3] //= pl _; rewrite fitp_catrev /= Dnf => /and3P[_ Ds _]; rewrite [in RHS](Dfn Ds) ?faceK ?Dnf. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry part quiz quiztree)