proposition: Lemma on_top_mergel m n (c1 : configuration m) (c2 : configuration n) d : cdisjoint c1 c2 -> on_top d c1 -> on_top (tlshift n d) (cmerge c1 c2).
proof: Proof. move=> c1Dc2 /on_topP dTc; apply/on_topP => d1. rewrite !ffunE tsplit_tlshift /=. case: tsplitP => j -> c1dc1j; last first. by rewrite leq_add2r; apply: dTc. by have /cdisjointP/(_ d j)/eqP[] := c1Dc2. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)