feat(data/nat/enat): is_well_order instance for enat (#14416)

src/data/nat/enat.lean

@@ -477,11 +477,15 @@ noncomputable def with_top_add_equiv : enat ≃+ with_top ℕ :=
 
 end with_top_equiv
 
-lemma lt_wf : well_founded ((<) : enat → enat → Prop) :=
-show well_founded (λ a b : enat, a < b),
-by haveI := classical.dec; simp only [to_with_top_lt.symm] {eta := ff};
-    exact inv_image.wf _ (with_top.well_founded_lt nat.lt_wf)
+lemma lt_wf : @well_founded enat (<) :=
+begin
+  classical,
+  change well_founded (λ a b : enat, a < b),
+  simp_rw ←to_with_top_lt,
+  exact inv_image.wf _ (with_top.well_founded_lt nat.lt_wf)
+end
 
+instance : is_well_order enat (<) := ⟨lt_wf⟩
 instance : has_well_founded enat := ⟨(<), lt_wf⟩
 
 section find