rw [List.prod_cons] at h
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]
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]