proposition: Lemma last_ppeg n p1 p2 c (cs := ppeg p1 p2 : seq (configuration 3 n)) : last c cs = `c[p2].
proof: Proof. have HH := @rirr 3. rewrite /cs; elim: n p1 p2 c {cs} => //= [_ p2 c | n IH p1 p2 c]. by apply/ffunP=> [] []. by rewrite last_cat /= last_map IH perfect_liftr. Qed.
imports: mathcomp(all_ssreflect) hanoi(extra gdist ghanoi ghanoi3)