mathlib3

5e2e8048 - feat(order/bounded_order): `subrelation r s ↔ r ≤ s` (#15357)

feat(order/bounded_order): `subrelation r s ↔ r ≤ s` (#15357) We have to place the lemma here, since comparing relations requires `has_le Prop`. I haven't made any judgement on whether either of them should be a simp-normal form.