Distrib lattice constructors

Stream: Is there code for X?

[Bhavik Mehta]

Is there a constructor for distrib_lattice using this distributive law:
x ⊓ (y ⊔ z) ≤ (x ⊓ y) ⊔ (x ⊓ z) instead of the one given there - it's mentioned that they're equivalent but only one is provided seemingly?

[Yury G. Kudryashov]

Is it the same as order_dual.distrib_lattice?

[Yury G. Kudryashov]

I mean, there is no constructor using this law now but probably you can write something like letI : distrib_lattice (order_dual α) := { .. order_dual.lattice, your_lemma }; exact { sup := ...; (other operations); .. show distrib_lattice (order_dual $ order_dual α), by apply_instance }.

[Yury G. Kudryashov]

Though possibly a better approach is to prove some iff or tfae for a lattice.