proposition: Lemma on_top_mergel_inv m n (c1 : configuration m) (c2 : configuration n) d : on_top (tlshift n d) (cmerge c1 c2) -> on_top d c1.
proof: Proof. move=> /on_topP dTc; apply/on_topP => d1 Hc. have := dTc (tlshift n d1). by rewrite !ffunE !tsplit_tlshift /= leq_add2r; apply. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)