Commit 2021-09-18 20:45 811c87ae

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.