For every non-negative integer n, the product (2n)*(2n+1)*(2n+2) of three consecutive integers starting at an even number is divisible by 4.

Enuntiatio — the claim

For every non-negative integer n, the product (2n)*(2n+1)*(2n+2) of three consecutive integers starting at an even number is divisible by 4.

Refuted by Some non-negative integer n makes (2n)*(2n+1)*(2n+2) leave a nonzero remainder when divided by 4.

Expressio — the formal statement

import Mathlib

theorem prod_three_consec_div_four (n : Nat) : (2*n)*(2*n+1)*(2*n+2) % 4 = 0

Demonstratio — the kernel-checked proof

by
  have h : (2*n)*(2*n+1)*(2*n+2) = 4 * (n*(2*n+1)*(n+1)) := by ring
  rw [h]
  omega