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