proposition: Lemma move_mergel m n (c1 c2 : configuration m) (c : configuration n) : move (cmerge c1 c) (cmerge c2 c) -> move c1 c2.
proof: Proof. move=> /moveP [x [H1x H2x H3x H4x]]; apply/moveP. move: H1x; rewrite !ffunE. case: tsplitP => [j | k kE J1x]; first by rewrite irH. have xE : (tlshift n k) = x by apply/val_eqP/eqP. rewrite -xE in H3x H4x. exists k; split => //; try by apply: on_top_mergel_inv; eassumption. move=> d2 kDd2. have := H2x (tlshift n d2). rewrite !ffunE tsplit_tlshift => H. apply: H. apply: contra kDd2 => /eqP/val_eqP /=. by rewrite kE eqn_add2r. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)