cmp
This commit also shows that nat.cmp is an instance of has_strict_weak_ordering.
to_unfold
simplify
simp*