example (x : Nat) : x + 1 > 0 := by
  induction x
  decide
  --^ $/lean/plainGoal