proposition: Lemma gdist_lhanoi3p n (p1 p2 : peg 3) : `d[`c[p1, n], `c[p2, n]]_lmove = if lrel p1 p2 then (3 ^ n).-1./2 else (3 ^ n).-1 * (p1 != p2).
proof: Proof. by rewrite gdist_lhanoi3_size size_lhanoi3_p. Qed.
imports: mathcomp(all_ssreflect) hanoi(gdist ghanoi ghanoi3)