mathlib4#792

Stream: PR reviews

[Scott Morrison]

I'm doing most of the merges for porting PRs, so when I occasionally do a port myself I need to flag it for someone to merge. :-)

Could someone please look over mathlib4#792, which ports Order.PropInstances. It is straightforward, with no porting notes.