## 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