| 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 | |
| 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 | |