Commit 2020-09-10 16:46 e33a777d
View on Github →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.