proposition: Lemma path_ppeg n p1 p2 (cs := ppeg p1 p2 : seq (configuration 3 n)) : p1 != p2 -> path rmove `c[p1] cs.
proof: Proof. have HH := @rirr 3. rewrite /cs; elim: n p1 p2 {cs} => //= n IH p1 p2 p1Dp2. set p3 := `p[_,_]. have p1Dp3 : p1 != p3 by rewrite eq_sym opegDl. have p3Dp2 : p3 != p2 by rewrite opegDr. rewrite cat_path /= -{1}[`c[p1]]cunliftrK ffunE !path_liftr // perfect_unliftr. rewrite !IH // ?andbT /=. rewrite -{1}[`c[_]]cunliftrK ffunE last_map perfect_unliftr last_ppeg. by apply: move_liftr_perfect; rewrite // eq_sym opegDr. Qed.
imports: mathcomp(all_ssreflect) hanoi(extra gdist ghanoi ghanoi3)