feat(data/nat/enat): derive typeclasses about well founded (#16346)

src/data/nat/enat.lean

@@ -17,14 +17,15 @@ about this type.
 @[derive [has_zero, add_comm_monoid_with_one, canonically_ordered_comm_semiring, nontrivial,
   linear_order, order_bot, order_top, has_bot, has_top, canonically_linear_ordered_add_monoid,
   has_sub, has_ordered_sub, complete_linear_order, linear_ordered_add_comm_monoid_with_top,
-  succ_order]]
+  succ_order, well_founded_lt, has_well_founded]]
 def enat : Type := with_top ℕ
 
 notation `ℕ∞` := enat
 
 namespace enat
 
 instance : inhabited ℕ∞ := ⟨0⟩
+instance : is_well_order ℕ∞ (<) := { }
 
 variables {m n : ℕ∞}