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