mathlib

3366a685 - feat(data/fin): eq_zero_or_eq_succ (#9136)

feat(data/fin): eq_zero_or_eq_succ (#9136) Particularly useful with `rcases i.eq_zero_or_eq_succ with rfl|⟨j,rfl⟩`. Perhaps it not worth having as a separate lemma, but it seems to avoid breaking the flow of a proof I was writing.