theorem ENat.tsum_const_eq' {α : Type u_1} (s : Set α) (c : ℕ∞) : ∑' (x : ↑s), c = s.encard * c