Theorem galois_coinsertion.is_coatom_iff'

feat(order/atoms): Galois (co)insertions and (co)atoms (#16663)