proposition: Lemma gdist_cshift n m (c1 c2 : configuration (m + n)) : connect move c1 c2 -> `d[clshift c1, clshift c2]_move + `d[crshift c1, crshift c2]_move <= `d[c1, c2]_move.
proof: Proof. move=> /gpath_connect[p pH]. rewrite (gpath_dist pH) (path_shift (gpath_path pH)). apply: leq_add. apply: gdist_path_le; first by apply/path_clshift/(gpath_path pH). by rewrite last_rm_rep last_map (gpath_last pH). apply: gdist_path_le; first by apply/path_crshift/(gpath_path pH). by rewrite last_rm_rep last_map (gpath_last pH). Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)