Commit 2021-11-09 09:20 86146152
View on Github →refactor(data/nat/interval): simp for Ico_zero_eq_range (#10211)
This PR makes two changes: It refactors nat.Ico_zero_eq_range from Ico 0 a = range a to Ico 0 = range, and makes the lemma a simp lemma.
These changes feel good to me, but feel free to close this if this is not the direction we want to go with this lemma.