no goals
ι : Type u_1
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : Zero α
inst✝ : LocallyFiniteOrder α
f g : ι →₀ α
⊢ card (Ioo f g) = ∏ i in f.support ∪ g.support, card (Icc (↑f i) (↑g i)) - 2
rw [card_Ioo_eq_card_Icc_sub_two, card_Icc]