proposition: Lemma gdist_plift (c1 c2 : configuration q n) : connect (move r1) c1 c2 -> `d[plift c1, plift c2]_(move r2) <= `d[c1, c2]_(move r1).
proof: Proof. move=> /gpath_connect [p1 p1H]. rewrite (gpath_dist p1H) -(size_map plift). apply: gdist_path_le; first by rewrite plift_path (gpath_path p1H). by rewrite last_map (gpath_last p1H). Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)