Description: Strong (or "total") induction principle over the finite ordinals. (Contributed by Scott Fenton, 17-Jul-2015) (Proof shortened by BJ, 16-Oct-2024)