# Zulip Chat Archive

## Stream: new members

### Topic: Recursively prove

#### AHan (Nov 03 2018 at 08:19):

Sorry, this might seems to be stupid, but I just can't figure out how to prove the problem inductively....

```
lemma add_nat_ge_self {a : ℕ} (b : ℕ) : a + b ≥ b :=
match b with
| 0 := begin simp, apply nat.zero_le end
| succ n := sorry
```

#### Mario Carneiro (Nov 03 2018 at 09:40):

In lean we write inductive definitions by pattern matching in the definition itself, not using match blocks like coq

#### Mario Carneiro (Nov 03 2018 at 09:41):

lemma add_nat_ge_self {a : ℕ} : ∀(b : ℕ), a + b ≥ b | 0 := begin simp, apply nat.zero_le end | (succ n) := sorry

#### Mario Carneiro (Nov 03 2018 at 09:42):

at the `sorry`

you should now have access to `add_nat_ge_self`

which you can apply recursively

#### Bryan Gin-ge Chen (Nov 03 2018 at 13:37):

What Mario wrote is cleaner but I want to point out that the following is probably what you were going for:

lemma add_nat_ge_self {a : ℕ} (b : ℕ) : a + b ≥ b := match a, b with | a, 0 := begin simp, apply nat.zero_le end | a, (nat.succ n) := sorry end

#### Mario Carneiro (Nov 03 2018 at 13:39):

well if you write it like that you won't be able to fill in the `sorry`

because you don't have access to the recursive function

#### Bryan Gin-ge Chen (Nov 03 2018 at 13:54):

It's there, but it gets a funny name:

lemma add_nat_ge_self {a : ℕ} (b : ℕ) : a + b ≥ b := match a, b with | a, 0 := begin simp, apply nat.zero_le end | a, (nat.succ n) := begin refine nat.succ_le_succ _, exact _match a n end end

#### Bryan Gin-ge Chen (Nov 03 2018 at 14:02):

And I guess you only get access to it if you go into tactic mode; i.e. I can't remove the `by exact`

below:

lemma add_nat_ge_self {a : ℕ} (b : ℕ) : a + b ≥ b := match a, b with | a, 0 := begin simp, apply nat.zero_le end | a, (nat.succ n) := nat.succ_le_succ (by exact _match a n) end

#### AHan (Nov 04 2018 at 03:59):

Oh!! Thanks a lot for the explanation!!

Last updated: May 08 2021 at 05:14 UTC