import Mathlib.Tactic

theorem consec_triple_div_by_3 (n : Nat) : 3 ∣ n * (n + 1) * (n + 2) := by
  intro n
  omega