no goals
⊢ WellFounded fun x x_1 => x < x_1
classical
  change WellFounded fun a b : PartENat => a < b
  simp_rw [← withTopEquiv_lt]
  exact InvImage.wf _ (WithTop.wellFounded_lt Nat.lt_wfRel.wf)
⊢ WellFounded fun a b => a < b
⊢ WellFounded fun x x_1 => x < x_1
change WellFounded fun a b : PartENat => a < b
⊢ WellFounded fun a b => ↑withTopEquiv a < ↑withTopEquiv b
⊢ WellFounded fun a b => a < b
simp_rw [← withTopEquiv_lt]
no goals
⊢ WellFounded fun a b => ↑withTopEquiv a < ↑withTopEquiv b
exact InvImage.wf _ (WithTop.wellFounded_lt Nat.lt_wfRel.wf)