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