proposition: Lemma cunliftrK n (c : configuration n.+1) : ↑[↓[c]]_(c ldisk) = c.
proof: Proof. apply/ffunP => i; rewrite !ffunE. case: tsplitP => [] j iE; rewrite !ffunE; congr fun_of_fin; apply/val_eqP/eqP => //=. by rewrite iE; case: (j) => [] []. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)