Proving well founded recursion

Stream: lean4

[Ben]

I am playing with groups and order ATM. I am trying the following

def Nat.find_after (p: Nat → Prop) [DecidablePred p] (n: Nat) (H : ∃n', n' >= n → p n') : Nat :=
if p n then n else (Nat.find_after p (.succ n) H)

def Nat.find (p: Nat → Prop) [DecidablePred p] (H : ∃n, p n) : Nat := Nat.find_after p 0 H

inductive ExtendedNat
| Finite : Nat → ExtendedNat
| Infinite : ExtendedNat

def Order (T: Type) [Pow T Nat] [OfNat T 1] (t: T) : ExtendedNat :=
  if ∃n, t ^ n = 1 then .Finite (Nat.find (fun n => t ^ n = 1) _) else .Infinite

I think it's sound. Just need to pass it through Lean.

[Ben]

I have read the mathlib Nat.findand std WellFounded.fix but couldn't quite figure out how to use them in a simple way?

[Ben]

Is there a way I can take my current statements and fix the current issues

• Proving Nat.find_after using H as a termination condition
• Modifying H in to alter or add the antecedent n' > n
• Use the condition in if to pass to Nat.find (currently it doesn't like the underscore :( )