mathlib

43e84cdd - feat(data/fin/succ_pred): `fin` is an archimedean succ/pred order (#12792)

feat(data/fin/succ_pred): `fin` is an archimedean succ/pred order (#12792) Co-authored-by: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>