Well Ordered

$\mathbb{Z}$ is constructed out of Peano's axioms in mathlib4. It can also be constructed out of Ring Axioms, Order Axioms, and the Well-ordering Principle.

Here presents a proof in lean that $\mathbb{Z}$ constructed out of Peano's axioms satisfy properties of well-ordered ring.