Well-Ordering

A binary relation $<:A\to A\to \mathrm{Prop}$ is a well-ordering if there is a relation such that:

• $<$ is a irreflexive.
• $<$ is transitive.
• $<$ is total.
• $<$ is well-founded.