mathlib3

8a6a7933 - refactor(data/fin/basic): reformulate `fin.strict_mono_iff_lt_succ` (#14482)

refactor(data/fin/basic): reformulate `fin.strict_mono_iff_lt_succ` (#14482) Use `fin.succ_cast` and `fin.succ`. This way we lose the case `n = 0` but the statement looks more natural in other cases. Also add versions for `monotone`, `antitone`, and `strict_anti`.