proposition: Lemma pathS_restrict n (c : configuration n.+1) cs : path move c cs -> {cs'| [/\ path move ↓[c] cs', last ↓[c] cs' = ↓[last c cs] & size cs' <= size cs ?= iff (cs == [seq ↑[i]_(c ldisk) | i <- cs'])]}.
proof: Proof. elim: cs c => /= [c _|c1 cs IH c /andP[cMc1 /IH[cs1 [c1Pcs1 lccs1Mlc1cs S]]]]. by exists [::]; split; rewrite ?setd_id //; apply: leqif_refl; rewrite !eqxx. have [/eqP c1dEcd|c1dDcd] := boolP (c ldisk == c1 ldisk). exists (cunliftr c1 :: cs1); split=> //=. by rewrite move_unliftr // cMc1. by rewrite eqseq_cons c1dEcd cunliftrK eqxx. have -> : cunliftr c = cunliftr c1 by apply: move_ldisk. exists cs1; split=> //=. apply/leqifP; case: eqP=> [H|/= _]; last by rewrite ltnS S. by rewrite -[_.+1]/(size (c1 :: cs)) H size_map. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)