WellFoundedGT Nat

Stream: lean4

[Ka Wing Li]

Is it true that I cannot prove the following? I can prove one for WellFoundedLT ℕ though.

instance : WellFoundedGT ℕ where
  wf := by
    sorry

[Yaël Dillies]

Yes, this is false. Eg 0 < 1 < 2 < ...

[Kenny Lau]

import Mathlib

theorem not_wellFoundedGT_nat : ¬WellFoundedGT ℕ :=
  fun h ↦ h.induction (C := fun _ ↦ False) 0 fun n ih ↦ ih (n + 1) (Nat.lt_succ_self n)

[Ruben Van de Velde]

Yaël Dillies said:

Yes, this is false. Eg 0 > 1 > 2 > ...

... excuse me?

[Yaël Dillies]

:innocent:

[Ka Wing Li]

Oh thanks. I see what is going on.