proposition: Lemma gpath_cset22 c1 c2 cs : all (cvalid sd sp1) (c1 :: cs) -> all (cvalid (~: sd) sp2) (c1 :: cs) -> gpath (move rel1) c1 c2 cs -> `d[cset2 sd p1Isp1 c1, cset2 sd p1Isp1 c2]_(move rel2) + `d[cset2 (~: sd) p2Isp2 c1, cset2 (~: sd) p2Isp2 c2]_(move rel3) <= `d[c1,c2]_(move rel1).
proof: Proof. move=> cV1 cV2 gH. rewrite (gpath_dist gH). apply: gdist_cset22 => //; first apply: gpath_last gH. by apply: gpath_path gH. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)