proposition: Lemma move_mergel_inv m n (c1 c2 : configuration m) (c : configuration n) : cdisjoint c1 c -> cdisjoint c2 c -> move c1 c2 -> move (cmerge c1 c) (cmerge c2 c).
proof: Proof. move=> c1Dc c2Dc /moveP[x [H1x H2x H3x H4x]]; apply/moveP. exists (tlshift n x); split => //; try by apply/on_top_mergel. by rewrite !ffunE /= tsplit_tlshift. move=> d2; rewrite !ffunE; case: tsplitP => // k d2E H. apply: H2x => //; apply: contra H => /eqP->. by apply/eqP/val_eqP/eqP. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)