chore(*): move/add lemmas about `disjoint` (#5277)
* `set.disjoint_compl_left` and `set.disjoint_compl_right`:
- generalize to any `boolean_algebra`,
- move to `order/boolean_algebra`,
- drop `set.` prefix,
- make the argument implicit to follow the style of other lemmas in `order/boolean_algebra`
* add `set.disjoint_empty` and `set.empty_disjoint`
* add `disjoint_top` and `top_disjoint`, use in `set.disjoint_univ`and `set.univ_disjoint`.
