∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [inst_2 : CanonicallyOrderedAdd α]
  [inst_3 : OrderBot α] [inst_4 : LocallyFiniteOrder α] [inst_5 : DecidableEq ι] [inst_6 : DecidableEq α] (f : ι →₀ α),
  (Finset.Iio f).card = ∏ i ∈ f.support, (Finset.Iic (f i)).card - 1