proposition: Lemma gdist_rhanoi3 n (c1 c2 : _ _ n) : `d[c1, c2]_rmove = size_rhanoi3 c1 c2.
proof: Proof. apply/eqP; rewrite eqn_leq. rewrite [size_rhanoi3 _ _]size_rhanoi3E gdist_path_le //=; last 2 first. - by apply: path_rhanoi3. - by apply: last_rhanoi3. have /gpath_connect [p1 p1H] : connect rmove c1 c2 by apply: move_connect. rewrite (gpath_dist p1H) rhanoi3_min //; first apply: gpath_path p1H. by apply: gpath_last p1H. Qed.
imports: mathcomp(all_ssreflect) hanoi(extra gdist ghanoi ghanoi3)