mathlib3

0d2bc57a - refactor(data/fin/basic): reformulat `fin.strict_mono_iff_lt_succ`

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