proposition: Lemma gdist_perfect_le n (c : configuration 3 n) p : `d[c, `c[p]]_rmove <= (2^ n).-1.
proof: Proof. by rewrite gdist_size_rpeg; apply: size_rpeg_up. Qed.
imports: mathcomp(all_ssreflect) hanoi(extra gdist ghanoi ghanoi3)