mathlib3

5db7a188 - feat(data/nat/basic): add decidable_exists_lt deciding existence of a natural below a bound satisfying a predicate (#5864)

feat(data/nat/basic): add decidable_exists_lt deciding existence of a natural below a bound satisfying a predicate (#5864) Given a decidable predicate `P` on naturals it is decidable if there is a natural below any bound satisying the `P`. closes #5755