proposition: Lemma zdart_shiftl zi zp : zdart (zshiftl zi zp) = zmove zi (edge (node (zporg zp))).
proof: Proof. have sz0l: size_part p0l = arity x0 by rewrite Dp0l size_rev_part Ep0r nFx0. have zorg0l: zorg p0l = x0 by rewrite /zorg sz0l iter_face_arity. case: zp => zi' pl pr; case sz_pl: (size_part pl) => [|n]. rewrite -(finv_eq_can faceK); case: pl => // in sz_pl *. by congr (zmove zi _); rewrite /zorg size_drop_part sz0l subn1. by case: pl sz_pl => // [s h|h ?|h ? ?|h ? ? ?] [] *; rewrite /= faceK ?zorg0l. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry part quiz quiztree)