proposition: Lemma on_top_merger m n x (c1 : configuration m) (c2 : configuration n) : on_top (trshift m x) (cmerge c1 c2) = on_top x c2.
proof: Proof. apply/on_topP/on_topP. move=> Hx d2 cxEcd2. have := Hx (trshift m d2). by rewrite !ffunE !tsplit_trshift => /(_ cxEcd2). move=> H d; rewrite !ffunE tsplit_trshift /=. case: tsplitP => [j -> H1 | k -> _]. by apply: H. by apply: leq_trans (ltnW _) (leq_addl _ _). Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)