proposition: Lemma rpeg_ppeg n p1 p2 : p1 != p2 -> rpeg `c[p1, n] p2 = ppeg p1 p2.
proof: Proof. elim: n p1 p2 => //= n IH p1 p2 p1Dp2. by rewrite ffunE perfect_unliftr (negPf p1Dp2) !IH // eq_sym opegDl. Qed.
imports: mathcomp(all_ssreflect) hanoi(extra gdist ghanoi ghanoi3)