mathlib

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

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