# [isabelle] Help on Proof

Hello,
Can Isabelle do a proof for the following recursion:
a(0)=a(1)=a(2)=1; a(n)=((n^3 - 6 n^2 + 12 n - 7)*a(n - 3) + (-3 n^3 + 15 n^2
- 25 n + 14)*
a(n - 2) + (3 n^3 - 12 n^2 + 15 n - 6)*a(n - 1))/(n (n - 1) (n - 2))
Prove that, for all n ≥ 1, abs(a(n)-(n+1)/3) < 2/(sqrt(3n)).
Unfortunately, I don't have the bandwidth to download the software; it would
be greatly appreciated if somebody could input this into Isabelle and email
me the output.
Thanks,
Howard

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*