## Stream: general

### Topic: missing lemmas for inf?

#### Johan Commelin (Jul 29 2019 at 20:16):

Both of these fail:

example (m n : ℕ) (h : m < n) : m = m ⊓ n := by library_search
example (m n : ℕ) (h : m < n) : m ≤ m ⊓ n := by library_search


#### Chris Hughes (Jul 29 2019 at 20:20):

I bet they work with le

#### Chris Hughes (Jul 29 2019 at 20:21):

Instead of lt

#### Johan Commelin (Jul 29 2019 at 20:34):

How much do you want to bet :stuck_out_tongue_wink:

#### Mario Carneiro (Jul 29 2019 at 23:01):

the equality is the other way around, I think this is inf_of_le_left. The second one is just a composition of this with le_of_eq

Last updated: May 08 2021 at 19:11 UTC