induction xs with
| nil => aesop
| cons y ys ih =>
  rw [List.prod_cons] at h
  cases hx with
  | head => exact Nat.ModEq.of_mul_right _ h
  | tail w hw =>
    exact ih (Nat.ModEq.of_mul_left _ h) hw
a b : ℕ
xs : List ℕ
h : a ≡ b [MOD xs.prod]
x : ℕ
hx : x ∈ xs
⊢ a ≡ b [MOD x]
no goals