proposition: Lemma gpath_cset2 c1 c2 cs : all cvalid (c1 :: cs) -> gpath (move rel1) c1 c2 cs -> `d[cset2 c1, cset2 c2]_(move rel2) <= `d[c1, c2]_(move rel1).
proof: Proof. move=> cV gH. rewrite (gpath_dist gH); apply: gdist_cset2 => //; first apply: gpath_last gH. by apply: gpath_path gH. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)