Commit 2026-02-22 16:37 7f14c970
View on Github →chore(Order/Monotone/Basic): use to_dual (#35648)
This PR uses to_dual on a few lemmas about Monotone.
I also turn some uses of to_dual into to_dual none, because these were made by me before to_dual none existed.