no goals
n : ℕ
a b : Fin n
⊢ card (Ici a) = n - ↑a
cases n with
| zero => exact Fin.elim0 a
| succ =>
  rw [← card_map, map_valEmbedding_Ici, Nat.card_Icc, Nat.succ_sub_one]
  assumption
no goals
case zero
a b : Fin Nat.zero
⊢ card (Ici a) = Nat.zero - ↑a
exact Fin.elim0 a
case succ.b
n✝ : ℕ
a b : Fin (Nat.succ n✝)
⊢ Fin (Nat.succ n✝)
case succ
n✝ : ℕ
a b : Fin (Nat.succ n✝)
⊢ card (Ici a) = Nat.succ n✝ - ↑a
rw [← card_map, map_valEmbedding_Ici, Nat.card_Icc, Nat.succ_sub_one]
no goals
case succ.b
n✝ : ℕ
a b : Fin (Nat.succ n✝)
⊢ Fin (Nat.succ n✝)
assumption