proposition: Lemma zproper_shiftl zi zp : zproper (zshiftl zi zp) = if zi is Znil then false else true.
proof: Proof. by case: zp => [_ pl pr] /=; case: pl => //= [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)