Using well-defined induction in Chapter 2

Stream: Analysis I

[Rado Kirov]

This is a question from the SF working group that we do weekly - @Chris Bailey showed us how to do well-founded induction in Lean - https://gist.github.com/ammkrn/98a2a3005b7d5613b8d71a9e12ce35a5#file-gistfile1-txt-L23 but we were not sure which proof would be closer to a canonical pen-and-paper one (as much as such one existst).