feat(order/bounded_lattice): add some disjoint lemmas (#8407)
This adds `disjoint.inf_left` and `disjoint.inf_right` (and primed variants) to match the existing `disjoint.sup_left` and `disjoint.sup_right`.
This also duplicates these lemmas to use set notation with `inter` instead of `inf`, matching the existing `disjoint.union_left` and `disjoint.union_right`.
