proposition: Lemma on_top_shift m n (c : configuration (m + n)) d : on_top d c -> match tsplit d with | inl d1 => on_top d1 (clshift c) | inr d2 => on_top d2 (crshift c) end.
proof: Proof. rewrite -{1}[d](tsplitK d). case: tsplitP => /= j dE /on_topP /= dT; apply/on_topP => d1; rewrite !ffunE /= => H. by apply: dT H. by have /= := dT _ H; rewrite leq_add2r. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)