Simple example of `decreasing_by` for Ordering matching

Stream: new members

[Alex Ness]

Hi everyone,

I have the following working definition:

/- Given a natural number n, return 0 by iterated subtraction. -/
def myZero (a : ℕ) : ℕ :=
  match a with
  | 0 => 0
  | a + 1 => myZero a

I would like the following equivalent definition:

def myZeroOrd (a : ℕ) : ℕ :=
  match compareOfLessAndEq a 0 with
  | lt => 0
  | eq => 0
  | gt => myZeroOrd (a - 1)
  decreasing_by {
    sorry
  }

How do I fill in the sorry here? Thanks for your help.

[Joachim Breitner]

Just a start, but if you write match h : you get a hypothesis into scope that may help you in the proof. Not saying it'll be pretty through, mere possible.

[Alex Ness]

@Joachim Breitner Thanks for the response. Can you show me explicitly what you mean? As a beginner it would be helpful for me to see the code.

[Kevin Buzzard]

Put h : after match and before all the other things and then you'll have h in your context

[Alex Ness]

@Kevin Buzzard Aha, that's clearer, thanks. I'll see what I can do from there.

[Joachim Breitner]

(please excuse my brevity, I was responding from the phone.)