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