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