search

albertqjiang / miniF2F

An updated version of miniF2F with problems fixed
0 stars 0 forks source link

[Lean Metamath Fix] imo_1974_p5 #37

Closed DyeKuu closed 2 years ago

DyeKuu commented 2 years ago

Note:

Add all positive constraints. In fact, the statement is a weaker version: we are not required to prove that s fulfill the range.