proposition: Lemma gpath_cut_tuc c1 c2 cs : gpath (move rel) c1 c2 cs -> `d[ccut c1, ccut c2]_(move rel) + `d[ctuc c1, ctuc c2]_(move rel) <= `d[c1,c2]_(move rel).
proof: Proof. move=> gH. rewrite (gpath_dist gH). apply: gdist_cut_tuc => //; first apply: gpath_last gH. by apply: gpath_path gH. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)