File size: 162 Bytes
fc2d127 | 1 2 3 4 5 6 7 8 9 10 | 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
|
fc2d127 | 1 2 3 4 5 6 7 8 9 10 | 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
|