proposition: Lemma gdist_cunlift n (c1 c2 : configuration n.+1) : connect move c1 c2 -> `d[↓[c1], ↓[c2]]_move <= `d[c1, c2]_move.
proof: Proof. by move=> H; apply: gdist_crshift. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)