feat(algebra/bounds): add `csupr_mul` etc (#8584)
* add `csupr_mul`, `mul_csupr`, `csupr_div`, `csupr_add`,
`mul_csupr`, `add_csupr`, `csupr_sub`;
* add `is_lub_csupr`, `is_lub_csupr_set`, `is_glb_cinfi`,
`is_glb_cinfi_set`;
* add `is_lub.csupr_eq`, `is_lub.csupr_set_eq`, `is_glb.cinfi_eq`,
`is_glb.cinfi_set_eq`;
* add `is_greatest.Sup_mem`, `is_least.Inf_mem`;
* add lemmas about `galois_connection` and `Sup`/`Inf` in
conditionally complete lattices;
* add lemmas about `order_iso` and `Sup`/`Inf` in conditionally
complete lattices.
