proposition: Lemma tsplit_tlshift k m (x : 'I_k) : tsplit (tlshift m x) = inl x.
proof: Proof. case: tsplitP=> [j /= jE|k1 /= /eqP]. by have := ltn_ord j; rewrite -jE ltnNge leq_addl. rewrite eqn_add2r => /eqP H. by congr (inl _); apply: val_inj. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)