proposition: Lemma path3SP n (c : _ _ n.+1) cs : path3S_spec c cs (path hmove c cs).
proof: Proof. case: pathSP=> //; try by constructor. move=> p1 p2 cs1 cs2 c1 c2 p1Dp2 p1Rp2 csE c1Pcs1 lMc2 c2Pcs2. have lc1cs1E : last c1 cs1 = `c[`p[p1, p2]]. have := move_perfectl lMc2. by rewrite !cliftr_ldisk cliftrK; apply. apply: path3S_spec_move (lc1cs1E) _ _ _ => //. - by rewrite csE; congr (_ ++ cliftr _ _ :: _). by rewrite -lc1cs1E. Qed.
imports: mathcomp(all_ssreflect) hanoi(ghanoi gdist)