ι : Type ?u.112982
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ c a b : α
⊢ card (Icc a b) - 1 - 1 = card (Icc a b) - 2
ι : Type ?u.112982
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ c a b : α
⊢ card (Ioo a b) = card (Icc a b) - 2
rw [card_Ioo_eq_card_Ico_sub_one, card_Ico_eq_card_Icc_sub_one]
no goals
ι : Type ?u.112982
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ c a b : α
⊢ card (Icc a b) - 1 - 1 = card (Icc a b) - 2
rfl