import Mathlib

/- Original: is = 12 − s -/
theorem eq_db937c0f244fb14f (is : ℕ) (s : ℕ) : is = 12 - s := by
  omega

