Commit 2022-07-15 07:02 5e2e8048

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.