proposition: Lemma zpvalid_shiftr zi zp : zpvalid zp -> zpvalid (zshiftr zi zp).
proof: Proof. case: zp => [_ pl pr] /=; move: zvalid_init zvalid_initr. by case: 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)