Zulip Chat Archive
Stream: new members
Topic: split off three
Daniel Selsam (Mar 12 2022 at 00:58):
Is something like the following somewhere in mathlib?
lemma split_off_three : ∀ (i n : ℕ), i < n + 3 ↔ i < n ∨ i = n ∨ i = n+1 ∨ i = n+2
Eric Rodriguez (Mar 12 2022 at 01:20):
interval_cases and fin_cases may help
Yaël Dillies (Mar 12 2022 at 09:21):
simp_rw nat.lt_succ_iff_lt_or_eq (docs#nat.lt_succ_iff_lt_or_eq)
Last updated: Dec 20 2023 at 11:08 UTC