Commit 2022-07-11 02:42 e3e4cc66

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.