case pos
ι : Type ?u.110964
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ c a b : α
h : a ≤ b
⊢ card (Ico a b) = card (Icc a b) - 1

case neg
ι : Type ?u.110964
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ c a b : α
h : ¬a ≤ b
⊢ card (Ico a b) = card (Icc a b) - 1
ι : Type ?u.110964
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ c a b : α
⊢ card (Ico a b) = card (Icc a b) - 1
by_cases h : a ≤ b
case pos
ι : Type ?u.110964
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ c a b : α
h : a ≤ b
⊢ card (Ico a b) = card (Ico a b) + 1 - 1
case pos
ι : Type ?u.110964
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ c a b : α
h : a ≤ b
⊢ card (Ico a b) = card (Icc a b) - 1
rw [Icc_eq_cons_Ico h, card_cons]
no goals
case pos
ι : Type ?u.110964
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ c a b : α
h : a ≤ b
⊢ card (Ico a b) = card (Ico a b) + 1 - 1
exact (Nat.add_sub_cancel _ _).symm
no goals
case neg
ι : Type ?u.110964
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a✝ b✝ c a b : α
h : ¬a ≤ b
⊢ card (Ico a b) = card (Icc a b) - 1
rw [Ico_eq_empty fun h' => h h'.le, Icc_eq_empty h, card_empty, zero_tsub]