case a
a b✝ c b : ℕ
h : 0 < b
x : ℕ
⊢ x ∈ Icc a (b - 1) ↔ x ∈ Ico a b
a b✝ c b : ℕ
h : 0 < b
⊢ Icc a (b - 1) = Ico a b
ext x
no goals
case a
a b✝ c b : ℕ
h : 0 < b
x : ℕ
⊢ x ∈ Icc a (b - 1) ↔ x ∈ Ico a b
rw [mem_Icc, mem_Ico, lt_iff_le_pred h]