proposition: Lemma psi_leD a b : psi `[a + b] <= (psi `[a]).*2 + 2 ^ (b.-1).
proof: Proof. case: b => [|b]; first by rewrite addn0 -addnn -addnA leq_addr. rewrite -leq_double doubleD [_.+1.-1]/=. rewrite !psi_sint_phi -addSn -ltnS prednK ?phi_gt0 //. apply: leq_trans (phi_leD _ _) _. rewrite -{1}[phi (a.+1)]prednK ?phi_gt0 // doubleS. by rewrite expnS mul2n -prednDr ?double_gt0 ?expn_gt0. Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) hanoi(extra triangular phi)