proposition: Lemma rpeg_perfect n p : rpeg (`c[p]) p = [::] :> seq (configuration 3 n).
proof: Proof. elim: n => //= n IH. by rewrite ffunE eqxx perfect_unliftr IH. Qed.
imports: mathcomp(all_ssreflect) hanoi(extra gdist ghanoi ghanoi3)