mathlib3

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

#1032

Merged