Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-05-17 00:16 def48b06

View on Github →

feat(data/nat/basic): make decreasing induction eliminate to Sort (#1032)

  • add interface for decreasing_induction to Sort
  • make decreasing_induction a def
  • add simp tags and explicit type

Estimated changes

deleted theorem nat.decreasing_induction