Finite intervals of naturals

This file calculates the cardinality of intervals of natural numbers as sets.

@[simp]

theorem Set.ncard_Icc_nat (a b : ℕ) : (Icc a b).ncard = b + 1 - a

@[simp]

theorem Set.ncard_Ico_nat (a b : ℕ) : (Ico a b).ncard = b - a

@[simp]

theorem Set.ncard_Ioc_nat (a b : ℕ) : (Ioc a b).ncard = b - a

@[simp]

theorem Set.ncard_Ioo_nat (a b : ℕ) : (Ioo a b).ncard = b - a - 1

@[simp]

theorem Set.ncard_uIcc_nat (a b : ℕ) : (uIcc a b).ncard = (↑b - ↑a).natAbs + 1

@[simp]

theorem Set.ncard_Iic_nat (b : ℕ) : (Iic b).ncard = b + 1

@[simp]

theorem Set.ncard_Iio_nat (b : ℕ) : (Iio b).ncard = b