m : ℕ
h : 0 < m
⊢ range' (m - 1) (m - (m - 1)) = [m - 1]
m : ℕ
h : 0 < m
⊢ Ico (m - 1) m = [m - 1]
dsimp [Ico]
m : ℕ
h : 0 < m
⊢ range' (m - 1) (succ 0) = [m - 1]
m : ℕ
h : 0 < m
⊢ range' (m - 1) (m - (m - 1)) = [m - 1]
rw [tsub_tsub_cancel_of_le (succ_le_of_lt h)]
no goals
m : ℕ
h : 0 < m
⊢ range' (m - 1) (succ 0) = [m - 1]
simp [← Nat.one_eq_succ_zero]