proposition: Lemma size_app_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. elim: n p1 p2 => [p1 p2|n IH p1 p2] /=; first by rewrite if_same. rewrite !ffunE; case: eqP => [p1Ep2|/eqP p1Dp2]. by rewrite !perfect_unliftr size_map IH p1Ep2 eqxx lirr !muln0. rewrite !perfect_unliftr !fun_if !size_cat /= !size_cat /= !size_map. rewrite !IH eq_sym opegDl // opegDr //= !muln1. have Hd : (3 ^ n.+1).-1 = (3 ^ n).-1 + (3 ^ n).*2. rewrite expnS -[3 ^n]prednK ?expn_gt0 //. by rewrite mulnS /= doubleS !addnS mulSn mul2n. rewrite ![lrel p2 _]lsym. case: (boolP (lrel _ _)) => [Hrel1|Hrel1]; last first. rewrite [p2 == _]eq_sym p1Dp2 !muln1. rewrite expnS !mulSn addn0. by case: expn (expn_gt0 3 n) => // k _; rewrite !addnS addnA. case: (boolP (lrel _ _)) => [Hrel2|Hrel2]. rewrite !ifN. by rewrite Hd halfD /= odd_double andbF add0n doubleK prednK ?expn_gt0. by have := lrel3B p1Dp2; rewrite Hrel1 Hrel2 lsym. rewrite ifT; last by rewrite lsym; apply: lrel3ON. rewrite Hd halfD /= odd_double andbF add0n doubleK -addSnnS addnC. by rewrite prednK // expn_gt0. Qed.
imports: mathcomp(all_ssreflect) hanoi(gdist ghanoi ghanoi3)