Talk:Equality of Successors
Note that this is (in some form) proved in Minimally Inductive Set forms Peano Structure, as axiom P3.
Probably best to move that formulation into here, and link from here to there.
Care needs to be taken to ensure that it is confirmed that elements of the Minimally Inductive Set are indeed ordinals. This is I think demonstrated somewhere, it just needs to be hauled out and made explicit.
Also the notation "$n^+$" needs to be linked to and explained. --prime mover 09:02, 28 July 2012 (UTC)