proposition: Lemma path_liftrn n m p (c : configuration n) (cs : seq (configuration _)) : path move (cliftrn m p c) (map (cliftrn m p) cs) = path move c cs.
proof: Proof. exact: path_merger. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)