chore(order/galois_connection): golf (#9236)
* add `galois_insertion.is_lub_of_u_image`,
`galois_insertion.is_glb_of_u_image`,
`galois_coinsertion.is_glb_of_l_image`, and
`galois_coinsertion.is_lub_of_l_image`;
* get some proofs in `lift_*` from `order_dual` instances;
* this changes definitional equalities for `Inf` and `Sup` so that we can reuse the same `Inf`/`Sup` for a `conditionally_complete_lattice` later.
