proposition: Lemma last_rpeg n (c : configuration 3 n) p (cs := rpeg c p) : last c cs = `c[p].
proof: Proof. rewrite /cs; elim: n c p {cs} => /= [c p| n IH c p]. by apply/ffunP=> [] []. case: eqP => [Ho|/eqP Do]. by rewrite -{1}[c](cunliftrK) Ho last_map IH perfect_liftr. by rewrite last_cat /= last_map last_ppeg perfect_liftr. Qed.
imports: mathcomp(all_ssreflect) hanoi(extra gdist ghanoi ghanoi3)