proposition: Lemma gdist_rhanoi4 (n : nat) (p1 p2 : peg 4) : p1 != p2 -> `d[`c[p1, n], `c[p2, n]]_rmove = ϕ(n).
proof: Proof. by move=> p1Dp2; apply/eqP; rewrite eqn_leq gdist_leq // gdist_geq. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra gdist ghanoi ghanoi4 triangular phi rhanoi3 psi)