Posting even though correct just for feedback, etc.
$n_0,n_1$ are lower/upper bounds of true values for strong induction. Guess I could have used different values, like 2 and 3, or 1 and 2, but it is "arbitrary" so long as the entire range in question is covered.
Sequence $a_1,a_2,a_3,...,a_n$ defined by $a_1=1,a_2=2;a_n=a_{n-1}+a_{n-2},n\ge 3$. Prove for all $n\ge 1, a_n<(\frac{7}{4})^n:S(n)=a_n<(\frac{7}{4})^n$ $n_0=3,n_1=4;S(1),S(2),S(3)/S(n_0)/S(n-1),S(4)/S(n_1)/S(n)$(are true); $a_{n+1}=a_n+a_{n-1}<(\frac{7}{4})^n+a_{n-1}<(\frac{7}{4})^n+(\frac{7}{4})^{n-1}=(\frac{7}{4})((\frac{7}{4})^{n-1}+(\frac{7}{4})^{n-2})$ $=(\frac{7}{4})(\frac{7}{4})^n((\frac{7}{4})^{-1}+(\frac{7}{4})^{-2})=(\frac{7}{4})^{n+1}((\frac{7}{4})^{-1}+(\frac{7}{4})^{-2})<(\frac{7}{4})^{n+1}$
A sequence starting at $a_1$ and $a_2$ with recurrence $a_n=a_{n-1}+a_{n-2}$ has the (ordinary) generating function $$ g(x)=\sum_{n\ge 1} a_nx^n = x\frac{a_1+(a_2-a_1)x}{1-x-x^2}. $$ (From the general theory of rational generating functions it's obvious that the denominator is $1-x-x^2$. The numerator can be swiftly obtained by fitting the first 2 terms...) With the general decomposition into partial fractions we have $$ a_i = F_{i-2} a_1+F_{i-1}a_2 $$ where $F_0=0$, $F_1=1$ and $F_i= F_{i-1}+F_{i-2}$ are the usual Fibonacci numbers with $\sum_{i\ge 0}F_i x^i=x/(1-x-x^2)$. For these we have the well-known Binet formula $$ F_n=\frac{(1+\surd 5)^n-(1-\surd 5)^n}{2^n\sqrt{5}} % =[\phi^n-(-{\phi-1}]/\surd 5 % =[\phi^n-(-{\phi-1})^n]/\surd 5 =[\phi^n-(-)^n\frac{1}{\phi^n}]/\surd 5 $$ where $\phi=(1+\surd 5)/2\approx 1.618033 < 7/4$ is the golden ratio. An equivalent well-known formula is that $F_n=round( \phi^n/\surd 5$, which means $F_n\le \phi^n/\surd 5+1$. The combination if this is $$ a_i \le a_1 [1+\frac{\phi^{i-2}}{\surd 5}]+a_2[1+\frac{\phi^{i-1}}{\surd 5}] $$ $$ a_i \le a_1+a_2 +a_1\frac{\phi^{i-1}}{\phi\surd 5}+a_2\frac{\phi^{i-1}}{\surd 5} $$ $$ a_i \le a_1+a_2 +\phi^{i-1}[\frac{a_1}{\phi\surd 5}+\frac{a_2}{\surd 5}]. $$ For $a_1=1$, $a_2=2$ in particular we have $a_i=F_{i+1}$ and the Binet rounding formula applies ``as is''.