mathlib

86146152 - refactor(data/nat/interval): simp for Ico_zero_eq_range (#10211)

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.