mathlib

e33a777d - feat(data/fin): iffs about succ_above ordering (#4092)

feat(data/fin): iffs about succ_above ordering (#4092) New lemmas: `succ_above_lt_iff` `lt_succ_above_iff` These help avoid needing to do case analysis when faced with inequalities about `succ_above`.