## Stream: general

### Topic: induction

#### Johan Commelin (Jul 23 2018 at 12:22):

Occasionally I find myself having the goal \forall n, P n that I want to prove by induction. But (as a mathematician) I always allow myself to use P m for all m < n in the induction step. So I would like to rewrite my initial goal into \forall n m, m < n \to P m. Is a statement like that already in mathlib?

#### Kenny Lau (Jul 23 2018 at 12:24):

Occasionally I find myself having the goal \forall n, P n that I want to prove by induction. But (as a mathematician) I always allow myself to use P m for all m < n in the induction step. So I would like to rewrite my initial goal into \forall n m, m < n \to P m. Is a statement like that already in mathlib?

strong induction?

#### Johan Commelin (Jul 23 2018 at 12:25):

I don't know anything about strong induction. Is that the name for the thing I am talking about?

#### Kenny Lau (Jul 23 2018 at 12:26):

it's called strong induction.

#check @nat.strong_induction_on
-- nat.strong_induction_on :
--  ∀ {p : ℕ → Prop} (n : ℕ), (∀ (n : ℕ), (∀ (m : ℕ), m < n → p m) → p n) → p n


#### Chris Hughes (Jul 23 2018 at 16:06):

Read the section in TPIL on the equation compiler and the docs in mathlib on the equation compiler.

Last updated: May 14 2021 at 22:15 UTC