proposition: Lemma s2f_liftr n (c : configuration n.+1) (p : peg) : s2f ([set i | c i == p] :\ ord_max) = s2f [set i | cunliftr c i == p].
proof: Proof. apply/fsetP=> i. apply/imfsetP/imfsetP => [] [/= j]. rewrite !inE => /andP[jDn /eqP cjEp] jEi. have jLn : j < n. rewrite -val_eqE /= in jDn. by have := ltn_ord j; rewrite ltnS leq_eqVlt (negPf jDn). exists (Ordinal jLn) => //=; rewrite !inE ffunE; apply/eqP. by rewrite -cjEp; congr (c _); apply: val_eqP. rewrite inE ffunE => /eqP cjEp iEj; exists (trshift 1 j) => //. by rewrite !inE cjEp -val_eqE //= neq_ltn ltn_ord /=. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)