case a
a b c x : ℕ
⊢ x ∈ Ico (succ a) (succ b) ↔ x ∈ Ioc a b
a b c : ℕ
⊢ Ico (succ a) (succ b) = Ioc a b
ext x
no goals
case a
a b c x : ℕ
⊢ x ∈ Ico (succ a) (succ b) ↔ x ∈ Ioc a b
rw [mem_Ico, mem_Ioc, succ_le_iff, lt_succ_iff]