case a
a b c x : ℕ
⊢ x ∈ Ico (succ a) b ↔ x ∈ erase (Ico a b) a
a b c : ℕ
⊢ Ico (succ a) b = erase (Ico a b) a
ext x
no goals
case a
a b c x : ℕ
⊢ x ∈ Ico (succ a) b ↔ x ∈ erase (Ico a b) a
rw [Ico_succ_left, mem_erase, mem_Ico, mem_Ioo, ← and_assoc, ne_comm, @and_comm (a ≠ x),
  lt_iff_le_and_ne]