# Zulip Chat Archive

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