Commit 2024-06-25 13:18 c4f1cc8b

feat(Data/Real/EReal): add simp theorems involving the sum of ⊤ and x (#14102)

• Add the theorem top_add_of_ne_bot which states that for any extended real number x which is not ⊥, the sum of ⊤ and x is equal to ⊤.
• Add the theorem add_top_of_ne_bot which states that for any extended real number x which is not ⊥, the sum of x and ⊤ is equal to ⊤.
• Add the theorem add_pos which states that for any two extended real numbers a and b, if both a and b are greater than 0, then their sum is also greater than 0.
• Add the theorem mul_pos which states that the product of two positive extended real numbers is positive.
• Add the theorem add_top_iff_ne_bot which states that for any extended real number x, the sum of x and ⊤ is equal to ⊤ if and only if x is not ⊥.
• Add the theorem top_add_iff_ne_bot which states that for any extended real number x, the sum of ⊤ and x is equal to ⊤ if and only if x is not ⊥.

--