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.





leanprover-community/mathlib,leanprover-community/mathlib