import Mathlib.Tactic

def zarankiewicz_bound (n : ℕ) : ℕ := (n + 1) ^ 2 / 4

theorem bounded_zarankiewicz : ∀ n : Fin 100, zarankiewicz_bound n.val = (n.val + 1) ^ 2 / 4 := by decide