Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-05-14 18:15 ae8f197b

View on Github →

feat(data/nat/basic): decreasing induction (#1031)

feat(data/nat/basic): decreasing induction
feat(data/nat/basic): better proof of decreasing induction

Estimated changes

Modified src/data/nat/basic.lean

added theorem nat.decreasing_induction

modified theorem nat.lt_iff_add_one_le

modified theorem nat.zero_max