proposition: Lemma move_merger m n (c : configuration n) (c1 c2 : configuration m) : move (cmerge c c1) (cmerge c c2) = move c1 c2.
proof: Proof. apply/moveP/moveP => [] [d1 [H1d1 H2d1 H3d1 H4d1]]; last first. exists (trshift n d1); split => //; try by rewrite on_top_merger. by rewrite !ffunE /= tsplit_trshift. move=> d2; rewrite !ffunE; case: tsplitP => // k d2E H. apply: H2d1 => //; apply: contra H => /eqP->. by apply/eqP/val_eqP/eqP. move: H1d1; rewrite !ffunE. case: tsplitP => [j jE H1x|k _]; last by rewrite irH. have d1E : (trshift n j) = d1 by apply/val_eqP/eqP. rewrite -d1E in H3d1 H4d1. exists j; split => //; try by rewrite -(on_top_merger _ c). move=> d2 kDd2. have := H2d1 (trshift n d2). rewrite !ffunE tsplit_trshift => H. apply: H. apply: contra kDd2 => /eqP/val_eqP /=. by rewrite jE. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)