proposition: Lemma phi_deltaD n p : p <= n.+1 -> phi (delta n + p) = 1 + (n + p) * 2 ^ n - 2 ^ n.
proof: Proof. elim: n p => [|n IHn]; first by case => // [] [|p]. elim => [_|p IHp pLn]. rewrite !addn0 deltaS IHn // -addnBA; last first. by rewrite -[X in X <= _]mul1n leq_mul2r addnS orbT. rewrite -[X in _ + (_ - X)]mul1n -mulnBl addnS subn1 /=. rewrite addnn -muln2 -mulnA -expnS. rewrite -{1}[n]subn0 -subSS mulnBl mul1n addnBA //. by rewrite -[X in X <= _]mul1n leq_mul2r orbT. rewrite addnS phiS IHp 1?ltnW //. rewrite (_ : troot _ = n.+1). rewrite subnK. by rewrite addnS mulSn [X in _ = _ + X - _]addnC addnA addnK. by rewrite [_ + p]addSn mulSn addnC -addnA leq_addr. by apply/eqP; rewrite trootE leq_addr [delta _.+2]deltaS ltn_add2l. Qed.
imports: mathcomp(all_ssreflect) hanoi(triangular)