@[simp]

theorem List.prod_replicate_int {n : Nat} {a : Int} : (replicate n a).prod = a ^ n

theorem List.prod_append_int {l₁ l₂ : List Int} : (l₁ ++ l₂).prod = l₁.prod * l₂.prod

theorem List.prod_reverse_int (xs : List Int) : xs.reverse.prod = xs.prod