proposition: Lemma pathS_restrictD n (c : configuration n.+1) c1 cs : path move c cs -> c1 \in cs -> c1 ldisk != c ldisk -> {cs'| [/\ path move ↓[c] cs', last ↓[c] cs' = ↓[last c cs] & size cs' < size cs]}.
proof: Proof. move=> cPcs c1Ics c1dDcd. have [cs1 [H1 H2 H3]] := pathS_restrict cPcs. exists cs1; split => //. move/leqifP : H3; case: eqP => // cs1Ecs. case/eqP: c1dDcd. move: c1Ics; rewrite cs1Ecs => /mapP[x xIcs1 ->]. by rewrite cliftr_ldisk. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)