proposition: Lemma gdist_clmerge c1 c2 : `d[clmerge c1, clmerge c2]_smove <= `d[c1, c2]_(move (@lrel 3)).
proof: Proof. have /gpath_connect[pa1 pa1H] := move_lconnect3 c1 c2. rewrite (gpath_dist pa1H) -(size_map clmerge). apply: gdist_path_le; first by rewrite path_clmerge // (gpath_path pa1H). by rewrite [LHS]last_map (gpath_last pa1H). Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra star gdist lhanoi3 ghanoi ghanoi4 shanoi)