True ↔ ∀ r > 0, ∃ k, ∀ (I₁ I₂ : Fin r → ℕ), (∀ (i : Fin r), 0 < I₁ i ∧ I₁ i + k ≤ I₂ i + 1) → (∀ (i j : Fin r), i < j → I₂ i < I₁ j) → ¬Erdos930.IsPower (∏ i, ∏ m ∈ Finset.Icc (I₁ i) (I₂ i), m)