proposition: Lemma gdist_cset22 c1 c2 cs : all (cvalid sd sp1) (c1 :: cs) -> all (cvalid (~: sd) sp2) (c1 :: cs) -> last c1 cs = c2 -> path (move rel1) c1 cs -> `d[cset2 sd p1Isp1 c1, cset2 sd p1Isp1 c2]_(move rel2) + `d[cset2 (~: sd) p2Isp2 c1, cset2 (~: sd) p2Isp2 c2]_(move rel3) <= size cs.
proof: Proof. move=> cV1 cV2 cL cPcs. rewrite (size_cset2 cV1 cV2) //. apply: leq_add. apply: gdist_path_le; first by apply: path_cset2 rel2_compat _ _ _ _. by rewrite last_rm_rep last_map cL. apply: gdist_path_le; first by apply: path_cset2 rel3_compat _ _ _ _. by rewrite last_rm_rep last_map cL. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)