proposition: Lemma gdist_clshift n m (c1 c2 : configuration (m + n)) : connect move c1 c2 -> `d[clshift c1, clshift c2]_move <= `d[c1, c2]_move.
proof: Proof. move=> /gpath_connect[p pH]. have := size_rm_rep (clshift c1) [seq (clshift i) | i <- p]. rewrite (gpath_dist pH) size_map; move/(leq_trans _); apply. apply: gdist_path_le; first by apply/path_clshift/(gpath_path pH). by rewrite last_rm_rep last_map (gpath_last pH). Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)