a b : ℕ+
⊢ card (Icc a b) = card (Icc ↑a ↑b)
a b : ℕ+
⊢ card (Icc a b) = ↑b + 1 - ↑a
rw [← Nat.card_Icc]
a b : ℕ+
⊢ card (Icc a b) = card (map (Function.Embedding.subtype fun n => 0 < n) (Icc a b))
a b : ℕ+
⊢ card (Icc a b) = card (Icc ↑a ↑b)
erw [← Finset.map_subtype_embedding_Icc _ a b (fun c x _ hx _ hc _ => hc.trans_le hx)]
no goals
a b : ℕ+
⊢ card (Icc a b) = card (map (Function.Embedding.subtype fun n => 0 < n) (Icc a b))
rw [card_map]