import Mathlib.Tactic

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