Extended natural numbers form a complete linear order

This instance is not in Data.ENat.Basic to avoid dependency on Finsets.

ink

noncomputable instance instCompleteLinearOrderENat : CompleteLinearOrder ℕ∞

Equations

• instCompleteLinearOrderENat = inferInstanceAs (CompleteLinearOrder (WithTop ℕ))