mathlib

e3e4cc66 - feat(data/nat/basic): split `exists_lt_and_lt_iff_not_dvd` into `if` and `iff` lemmas (#15099)

feat(data/nat/basic): split `exists_lt_and_lt_iff_not_dvd` into `if` and `iff` lemmas (#15099) Pull out from `exists_lt_and_lt_iff_not_dvd` ("`n` is not divisible by `a` iff it is between `a * k` and `a * (k + 1)` for some `k`") a separate lemma proving the forward direction (which doesn't need the `0 < a` assumption) and use this to golf the `iff` lemma. Also renames the lemma to the more descriptive `not_dvd_{of,iff}_between_consec_multiples`.