proposition: Lemma perfect_liftrn m n p : cliftrn m p (`c[p]) = `c[p] :> configuration (m + n).
proof: Proof. by apply/ffunP => i; rewrite !ffunE; case: tsplitP => j; rewrite !ffunE. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist)