proposition: Lemma cliftr_ldisk n p (c : configuration n) : ↑[c]_p ldisk = p.
proof: Proof. rewrite ffunE; case: tsplitP => /= [j nE|t]. by have := ltn_ord j; rewrite {2}nE ltnn. by rewrite ffunE. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)