proposition: Lemma gdist_rhanoi3p n p1 p2 : `d[`c[p1, n], `c[p2]]_rmove = (2^ n).-1 * (p1 != p2).
proof: Proof. case: eqP => [<-|/eqP p1Dp2]; first by rewrite muln0 gdist0. rewrite muln1. apply/eqP; rewrite eqn_leq -(size_ppeg n p1 p2). rewrite gdist_path_le //=; last 2 first. - by apply: path_ppeg. - by rewrite last_ppeg. have /gpath_connect [cs csH] : connect rmove `c[p1, n] `c[p2]. by apply: move_connect_ppeg. rewrite size_ppeg (gpath_dist csH) /=. apply: ppeg_min p1Dp2 (gpath_path csH) _ => //. by apply: gpath_last csH. Qed.
imports: mathcomp(all_ssreflect) hanoi(extra gdist ghanoi ghanoi3)