import Mathlib.Tactic

theorem consec_prod_even (n : Nat) : 2 ∣ n * (n + 1) := by
  omega