basic): decreasing induction (#1031)

Commit

6 years ago

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

References

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

Author

sgouezel

Committer

mergify[bot]

Parents

e7b64c55

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

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