proposition: Lemma path_rpeg n (c : configuration 3 n) p (cs := rpeg c p) : path rmove c cs.
proof: Proof. have HH := @rirr 3. rewrite /cs; elim: n c p {cs} => //= n IH c p. case: eqP => [Ho|/eqP Do]. by rewrite -{1}[c](cunliftrK) Ho path_liftr. set c2 := `c[_]. rewrite cat_path /= -{1}[c]cunliftrK !path_liftr // IH path_ppeg ?opegDr //. rewrite andbT /=. rewrite -{1}[c]cunliftrK last_map last_rpeg -/c2. apply: move_liftr_perfect => //; first by rewrite eq_sym (opegDl _). by rewrite eq_sym (opegDr _). Qed.
imports: mathcomp(all_ssreflect) hanoi(extra gdist ghanoi ghanoi3)