# Zulip Chat Archive

## Stream: new members

### Topic: Induction on well founded relation

#### Pedro Minicz (Sep 25 2020 at 18:25):

I am suck in this seemingly innocuous proof:

```
lemma nat.div_two_mul_two (n : ℕ) : (n / 2) * 2 ≤ n :=
begin
induction n with n ih,
{ refl },
{ sorry }
end
```

My problem is: I don't know how to proceed. If `nat.div`

was defined using "normal" induction," I am pretty sure I would be able to unfold `n.succ / 2`

into something (hopefully) more useful. How to generally work with definitions that use `well_founded`

?

#### Pedro Minicz (Sep 25 2020 at 18:27):

I am not sure I understand even half of the definition of `nat.div`

. I'd love to know where I can read more about well founded relations. I know there is something in *Theorem Proving in Lean*, but not much.

#### Yakov Pechersky (Sep 25 2020 at 19:10):

You might like to look at `nat.le_div_iff_mul_le`

#### Yakov Pechersky (Sep 25 2020 at 19:10):

Which I found via just guessing the name `nat.div_mul_le_self`

#### Pedro Minicz (Sep 26 2020 at 00:51):

I managed to do what I wanted. It was basically a less general version of `nat.le_div_iff_mul_le`

. For future reference: `nat.strong_induction_on`

is pretty cool. :sunglasses:

Last updated: May 12 2021 at 22:15 UTC