proposition: Lemma move_clshift m n (c1 c2 : configuration (m + n)) : move c1 c2 -> (clshift c1) != (clshift c2) -> move (clshift c1) (clshift c2).
proof: Proof. move=> /moveP [x]. rewrite -(tsplitK x). have := @on_top_shift _ _ c1 x. have := @on_top_shift _ _ c2 x. case: tsplitP => /= [j xE c2H c1H [H1j H2j H3j H4j] c1Dc2| k xE c2H c1H [H1k H2k H3k H4k] c1Dc2]. case/eqP: c1Dc2; apply/ffunP => i. rewrite !ffunE. apply/H2j/eqP/val_eqP; rewrite eqn_leq /= negb_and. by rewrite orbC -ltnNge (leq_trans (ltn_ord _)) // leq_addl. apply/moveP; exists k; split=> [|d2 kDd2||]; rewrite ?ffunE //. - apply: H2k => /=. by apply/eqP/val_eqP; rewrite /= eqn_add2r; apply/val_eqP/eqP. - apply: c1H; rewrite (_ : x = (tlshift n k)) //. by apply/val_eqP/eqP => /=. apply: c2H; rewrite (_ : x = (tlshift n k)) //. by apply/val_eqP/eqP => /=. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)