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