Commit 2022-05-01 21:51 b236cb20
View on Github →chore(set_theory/surreal/basic): Inline instances (#13811)
We inline various definitions used only for instances. We also remove the redundant lemma not_le (which is more generally true on preorders).