mathlib3

7fbadc69 - chore(order/basic): move `Prop.partial_order` to `order/basic` (#15884)

chore(order/basic): move `Prop.partial_order` to `order/basic` (#15884) This ensures, among other things, that `r ≤ s` is almost always available as notation for subrelations. We don't move `Prop.linear_order` since doing so means we need to manually prove `or = max_default` and `and = min_default`.