## Big ops and lattices in stdpp?

Hi,

I currently have a meet-semilattice, and I want to show that if a map `m1`

is "less" than `m2`

, in the sense that `m1`

's values are pointwise less than those of `m2`

's by the lattice order, then the meet of `m1`

values is also less than that of `m2`

. I don't see a clean way to prove this, as I define the meet as a fold over the list of values.

I'd like a more structure way to define the meet as big ops in Iris. Is is possible to generalize big ops so that they need not depend on ofe's?

Also, I believe lattices would be useful enough to be in stdpp, although our development of them in iGPS is a bit under-developed.

What do you think?