As a computer scientists, I have been thought to use induction and coinduction principles for proving properties of finite and infinite structures, respectively.
When does one use ordinal induction? Since it is still induction, one cannot replace coinduction with ordinal one? In which cases one could not use induction and coinduction, and would have to resort to ordinal induction? How do these induction principles relate?
Formal and informal explanations are both welcomed.