[Agda] ⊓ in Nat

[Sergei Meshveliani]

Dear list,

This is on Standard library.

Data.Nat  defines _⊓_,  and Data.Nat.Properties proves certain
properties of _⊓_.
And I have an impression that it lacks a lemma

  ⊓≤both :  ∀ m n →  m ⊓ n ≤ m  ×  m ⊓ n ≤ n

Regards,

------
Sergei