proposition: Lemma gdist_liftrn n m p (c1 c2 : configuration n) : connect move c1 c2 -> `d[cliftrn m p c1, cliftrn m p c2]_move <= `d[c1, c2]_move.
proof: Proof. exact: gdist_merger. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)