proposition: Lemma gdist_lhanoi3_size n (c1 c2 : _ _ n) : `d[c1, c2]_lmove = size_lhanoi3 c1 c2.
proof: Proof. apply/eqP; rewrite eqn_leq [size_lhanoi3 _ _]size_lhanoi3E. rewrite gdist_path_le //=; last 2 first. - by apply: path_lhanoi3. - by apply: last_lhanoi3. have /gpath_connect[p1 p1H] : connect lmove c1 c2 by apply: move_lconnect3. rewrite (gpath_dist p1H) lhanoi3_min //; first by apply: gpath_path p1H. by apply: gpath_last p1H. Qed.
imports: mathcomp(all_ssreflect) hanoi(gdist ghanoi ghanoi3)