Induction on well founded relation

Stream: new members

[Pedro Minicz]

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]

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]

You might like to look at nat.le_div_iff_mul_le

[Yakov Pechersky]

Which I found via just guessing the name nat.div_mul_le_self

[Pedro Minicz]

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: