proposition: Lemma gdist_liftr n p (c1 c2 : configuration n) : connect move c1 c2 -> `d[↑[c1]_p, ↑[c2]_p]_move <= `d[c1, c2]_move .
proof: Proof. by apply: (@gdist_merger 1). Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)