mathlib3

b064622f - feat(data/fin/interval): Cardinality of `finset.Ixi`/`finset.Iix` in `fin` (#10168)

feat(data/fin/interval): Cardinality of `finset.Ixi`/`finset.Iix` in `fin` (#10168) This proves `(Ici a).card = n + 1 - a`, `(Ioi a).card = n - a`, `(Iic b).card = b + 1`, `(Iio b).card = b` where `a b : fin (n + 1)` (and also `a b : ℕ` for the last two).