cases hx with
| head => exact Nat.ModEq.of_mul_right _ h
| tail w hw =>
  exact ih (Nat.ModEq.of_mul_left _ h) hw
case cons
a b x y : ℕ
ys : List ℕ
ih : a ≡ b [MOD ys.prod] → x ∈ ys → a ≡ b [MOD x]
h : a ≡ b [MOD y * ys.prod]
hx : x ∈ y :: ys
⊢ a ≡ b [MOD x]
no goals