proposition: Lemma psi_SS_le n : psi `[n.+2] >= 2 ^(troot n).+1.
proof: Proof. case: n => [|n]; first by rewrite psi_sint2. have /psi_sint_leq/(leq_trans _)->// : (delta (troot n.+1)).+2 <= n.+3. by rewrite !ltnS -root_delta_le. set s := troot _. have [|tLs] := leqP s 1. case: s => [|[|]] //; first by rewrite psi_sint2 ?(leq_trans _ thLN). by rewrite psi_sint3. rewrite -leq_double psi_sint_phi phi_modSE. have tE : troot (delta s).+2 = s. by apply/eqP; rewrite trootE deltaS ltnW //= -addn2 addSnnS leq_add2l. rewrite tE. have->: tmod (delta s).+2 = 2 by rewrite /tmod tE -addn2 addnC addnK. by rewrite -mul2n expnS mulnA /= leq_mul2r (leq_add2r 2 2) tLs orbT. Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) hanoi(extra triangular phi)