proposition: Lemma move_crshift m n (c1 c2 : configuration (m + n)) : move c1 c2 -> (crshift c1) != (crshift c2) -> move (crshift c1) (crshift 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]; last first. case/eqP: c1Dc2; apply/ffunP => i. rewrite !ffunE. apply/H2k/eqP/val_eqP; rewrite eqn_leq /= negb_and. by rewrite -ltnNge (leq_trans (ltn_ord _)) // leq_addl. apply/moveP; exists j; split=> [|d2 kDd2||]; rewrite ?ffunE //. - by apply: H2j. - apply: c1H; rewrite (_ : x = (trshift m j)) //. by apply/val_eqP/eqP => /=. apply: c2H; rewrite (_ : x = (trshift m j)) //. by apply/val_eqP/eqP => /=. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)