feat(data/nat/basic): recursion for set nat (#10273)
feat(data/nat/basic): recursion for set nat (#10273)

Adding a special case of `nat.le_rec_on` where the predicate is membership of a subset.






leanprover-community/mathlib,leanprover-community/mathlib