nat.lt_iff_eq_succ

Stream: Is there code for X?

[Eric Wieser]

docs#nat.exists_eq_add_of_lt is close

[Eric Wieser]

docs#nat.exists_eq_succ_of_ne_zero is even better

[Eric Wieser]

I don't remember if we ever decided which of c ≠ 0 and 0 < c was the preferred spelling

[Eric Wieser]

So it pays to look for both for this type of thing

[Heather Macbeth]

In the measure theory library they have settled on "≠ in hypotheses, < in conclusions", which is somehow the best of both worlds.