I think it's fine. It's analogous to starting induction from 0 over the natural numbers.
It does feel a bit tricky though because there are two nested foralls instead of just one in standard induction. I think to derive it from standard induction you need to perform induction over sets of statements, which takes more power than first order logic. This additional power is generally accepted in math courses. It isn't necessary though, you can prove the irrationality of sqrt 2 using standard induction.
The article discussed how additional techniques can be made rigorous in the opening paragraph. I agree that the author didn't fully justify the assumptions in the proof system used, instead bringing this well ordered induction as an axiom. This is an article, I think a full aximization would have taken too long.
