graph TD
    A1["A1\n0 ∈ N"]
    A2["A2\n0 not a successor"]
    A3["A3\nS injective"]
    A4["A4\nN closed under S"]
    A5["A5\nInduction"]
    T1["T1\nContrapositive of A3"]
    T2["T2\nSuccessor ≠ identity"]
    T3["T3\nEvery nonzero is successor"]
    DefAdd["DefAdd\nDefinition of +"]
    T4["T4\nAdd well-defined"]
    T5["T5\nAssociativity of +"]
    T6["T6\nLeft identity"]
    T7["T7\nSuccessor and add"]
    T8["T8\nCommutativity of +"]
    T9["T9\nCancellation for +"]
    DefMul["DefMul\nDefinition of ·"]
    T10["T10\nMul well-defined"]
    T11["T11\nZero times"]
    T12["T12\nZero from left"]
    T13["T13\nSuccessor and mul"]
    T14["T14\nCommutativity of ·"]
    T15["T15\nAssociativity of ·"]
    T16["T16\nDistributivity"]
    T17["T17\nDistributivity (right)"]
    T18["T18\nOrder definition"]
    T19["T19\nTrichotomy"]
    T20["T20\nOrder + add"]
    T21["T21\nOrder + mul"]
    T22["T22\nMultiplicative identity"]
    T23["T23\nRight identity"]
    T24["T24\nWell-ordering"]
    T25["T25\nStrong induction"]
    A3 --> T1
    A1 --> T2
    A2 --> T2
    A3 --> T2
    T1 --> T2
    A5 --> T2
    A5 --> T3
    A5 --> DefAdd
    DefAdd --> T4
    A5 --> T4
    DefAdd --> T5
    A5 --> T5
    DefAdd --> T6
    A5 --> T6
    DefAdd --> T7
    T6 --> T7
    A5 --> T7
    DefAdd --> T8
    T5 --> T8
    T6 --> T8
    T7 --> T8
    A5 --> T8
    DefAdd --> T9
    T8 --> T9
    A5 --> T9
    DefAdd --> DefMul
    A5 --> DefMul
    DefMul --> T10
    A5 --> T10
    DefMul --> T11
    DefMul --> T12
    T6 --> T12
    A5 --> T12
    DefMul --> T13
    T8 --> T13
    A5 --> T13
    DefMul --> T14
    T12 --> T14
    T13 --> T14
    A5 --> T14
    DefMul --> T15
    T5 --> T15
    T8 --> T15
    A5 --> T15
    DefMul --> T16
    T5 --> T16
    T8 --> T16
    T15 --> T16
    A5 --> T16
    T16 --> T17
    T8 --> T17
    DefAdd --> T18
    T8 --> T18
    T9 --> T18
    T18 --> T19
    T9 --> T19
    T18 --> T20
    T8 --> T20
    T18 --> T21
    T16 --> T21
    T14 --> T21
    DefMul --> T22
    T6 --> T22
    A5 --> T22
    T14 --> T23
    T22 --> T23
    T18 --> T24
    T19 --> T24
    A5 --> T24
    T18 --> T25
    T24 --> T25
    A5 --> T25
    classDef axiom fill:#e74c3c,color:#fff,stroke:#c0392b
    classDef definition fill:#3498db,color:#fff,stroke:#2980b9
    classDef theorem fill:#1abc9c,color:#fff,stroke:#16a085
    class A1,A2,A3,A4,A5 axiom
    class DefAdd,DefMul definition
    class T1,T2,T3,T4,T5,T6,T7,T8,T9,T10,T11,T12,T13,T14,T15,T16,T17,T18,T19,T20,T21,T22,T23,T24,T25 theorem