namespace MiniF2F

theorem demo_nonneg_square (x : ℝ) : x ^ 2 ≥ 0 := by
  sorry

theorem demo_add_comm (a b : Nat) : a + b = b + a := by
  sorry

end MiniF2F
