Note: I'll be putting letters before each statement I discuss in order to easily reference them.
If I'm proving a statement with induction, can I use induction on a statement that I derive inside said proof? For example:
Prove for all positive integers n >= 3, that:
A: n! > ((n-1)! + (n-2)! + (n-3)!)
To solve this, I checked that the inequality holds for the base case n = 3, which it does. Then in the inductive step, I assumed the inequality was correct.
Before trying to prove the inequality for n+1, I algebraically simplified the assumption (A) into:
B: n^3 - 4n^2 + 4n - 1 > 0
And then my goal is to prove:
C: (n+1)^3 - 4(n+1)^2 + 4(n+1) - 1 > 0
Using assumption B, I simplified C into:
D: 3n^2 - 5n + 1 > 0
Now if I solve D, my entire proof is correct (i.e., I've proved A).
The problem is, I don't know how to prove D without using induction. So I used induction and was able to successfully prove D for all n >= 3.
My question is was I allowed to use a separate induction in the inductive step of the original proof?