proposition: Lemma gdist_merger m n (c: configuration m) (c1 c2 : configuration n) : connect move c1 c2 -> `d[cmerge c c1, cmerge c c2]_move <= `d[c1, c2]_move.
proof: Proof. move=> /gpath_connect[p1 p1H]. rewrite (gpath_dist p1H) -(size_map (cmerge c)). apply: gdist_path_le; first by rewrite path_merger (gpath_path p1H). by rewrite [LHS]last_map (gpath_last p1H). Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)