On Sat, 2017-04-22 at 20:35 +0200, Andreas Abel wrote: > Dear Sergei, > > well, there is > > m⊓n≤m : ∀ m n → m ⊓ n ≤ m > m⊓n≤m zero _ = z≤n > m⊓n≤m (suc m) zero = z≤n > m⊓n≤m (suc m) (suc n) = s≤s $ m⊓n≤m m n > > and there is commutativity of the minium. > [..] > Together, you get what you need. Indeed, I missed this name of m⊓n≤m. Thank you. ------ Sergei