proposition: Lemma zshiftl_eq zi zi' pl pr : 1 < size_part pl -> zshiftl zi' (Zpart zi pl pr) = Zpart zi' (drop_part 1 pl) (shift_part pl pr).
proof: Proof. by 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)