proposition: Lemma zdart_shiftr zi zp : zpvalid zp -> zdart (zshiftr zi zp) = zmove zi (face (zporg zp)).
proof: Proof. case: zp => zi' pl pr /(congr1 size_part). rewrite catrev_part_eq size_cat_part size_rev_part -iterS. case sz_pr: (size_part pr) => [|[|n]] sz_pl; rewrite ?addn0 ?addn1 in sz_pl. - rewrite {}sz_pl -zvalid_initr catrev_part_eq size_cat_part size_rev_part. rewrite size_drop_part subn1 Ep0r -nFx0 -addnS iterD [RHS]/=(f_finv faceI). by case: pr sz_pr. - rewrite {}sz_pl -zvalid_init catrev_part_eq size_cat_part size_rev_part. rewrite iterD Ep0r -nFx0 iter_face_arity. by case: pr sz_pr => // [s h|h f1|h f1 f2|h f1 f2 f3] []. by case: pr sz_pr => // [s h|h f1|h f1 f2|h f1 f2 f3] []. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry part quiz quiztree)