## Stream: maths

### Topic: decreasing induction

#### Sebastien Gouezel (Apr 09 2019 at 19:22):

I can not find the fact that, if a property P n holds and if P (i+1) implies P i for all i, then P m holds whenever m <= n. Is this already in mathlib?

Last updated: May 06 2021 at 19:30 UTC