Erdős Problem 7

Reference: erdosproblems.com/7

theorem Erdos7.erdos_7 : sorry ↔ ∃ (C : StrictCoveringSystem ℤ), ∀ (i : C.ι), ¬C.moduli i ≤ Ideal.span {2} ∧ C.moduli i ≠ ⊤

Is there a covering system all of whose moduli are odd (and greater than 1)?