proposition: Lemma zdart_stepRt zp : zpfit_top zp -> zpvalid zp -> zpfit (qstepR (zdart zp)) (zstepRt zp).
proof: Proof. case: zp => zi pl pr zp_top zp_ok; have /zdart_stepR := zp_ok. case: zi zp_ok zp_top => // zp_ok /eqP/Dfn/(congr1 (iter 4 (edge \o node))). rewrite /zpfit !zdart_shiftr ?zproper_shiftr {zp_ok}//= [qstepR _]Dne /zmove /=. by case: pr => // -[] // h pr; rewrite !faceK Dn3 Dnf !De2 => ->; rewrite Dnf. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry part quiz quiztree)