proposition: Lemma connect_liftrn n m p (c1 c2 : configuration n) : connect move c1 c2 -> connect move (cliftrn m p c1) (cliftrn m p c2).
proof: Proof. exact: connect_merger. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)