Erdős Problem 273

Reference: erdosproblems.com/273

theorem Erdos273.erdos_273 : sorry ↔ ∃ (c : StrictCoveringSystem ℤ), ∀ (i : c.ι), ∃ (p : ℕ), Nat.Prime p ∧ 5 ≤ p ∧ c.moduli i = Ideal.span {↑(p - 1)}

Is there a covering system all of whose moduli are of the form $p-1$ for some primes $p \geq 5$?

theorem Erdos273.erdos_273.variants.three : True ↔ ∃ (c : StrictCoveringSystem ℕ), ∀ (i : c.ι), ∃ (p : ℕ), Nat.Prime p ∧ 3 ≤ p ∧ c.moduli i = Ideal.span {p - 1}

Is there a covering system all of whose moduli are of the form $p-1$ for some primes $p \geq 3$?