Commit 2023-01-22 01:26 3fbdae49

feat: =, ≠, <, and ≤ functionality for norm_num (#1568) This PR gives norm_num basic inequality (and equality) functionality (towards #1567), including the following:

example {α} [DivisionRing α] [CharZero α] : (-1:α) ≠ 2 := by norm_num

We implement basic logical extensions to handle = and ≠ together, namely ¬, True, and False. ≠ is not given an extension, as it is handled by = and ¬. For now we only can prove ≠ for numbers given a CharZero α instance.

• depends on: #1578