proposition: Lemma gdist_shanoi4 (n : nat) (p1 p2 : peg 4) : p1 != p2 -> p1 != p0 -> p2 != p0 -> `d[`c[p1, n], `c[p2, n]]_smove = (S_[1] n).*2.
proof: Proof. move=> p1Dp2 p1Dp0 p2Dp0; apply/eqP; rewrite eqn_leq. by rewrite leq_shanoi4 // main_cor. Qed.
imports: mathcomp(all_ssreflect finmap) hanoi(extra star gdist lhanoi3 ghanoi ghanoi4 shanoi)