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