proposition: Lemma gdist_tuc c1 c2 cs : last c1 cs = c2 -> path (move rel) c1 cs -> `d[ctuc c1, ctuc c2]_(move rel) <= size cs.
proof: Proof. move=> cL cPcs. have := size_rm_rep (ctuc c1) [seq (ctuc i) | i <- cs]. rewrite size_map; move/(leq_trans _); apply. apply: gdist_path_le; first by apply: path_tuc. by rewrite last_rm_rep last_map cL. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)