[Agda] signature for `with' branch

[Sergei Meshveliani]

On Tue, 2017-02-28 at 16:00 +0100, Nils Anders Danielsson wrote:
> On 2017-02-28 12:49, Sergei Meshveliani wrote:
> > I knew that it is not reduced. But how to make it reduced there without
> > using `with' or `case' ?
> 
> Use regular pattern matching.
> 


Can anybody show, please, how to prove in Agda  

    lemma :  ∀ x y → x < y → min x y ≡ x

by using a regular pattern matching, and without using `with' or 'case'
?

min  is defined here:

-------------------------------------------------------------------
open import Function using (flip)
open import Relation.Binary using (Rel; Tri; StrictTotalOrder)
open import Relation.Binary.PropositionalEquality as PE using (_≡_)

module _ {α α= α<} (sto : StrictTotalOrder α α= α<)
  where
  open StrictTotalOrder sto using (_≈_; _<_; compare) 
                            renaming (Carrier to C)
  _>_ = flip _<_
  open Tri

  min : (x y : C) → C
  min x y =
          aux (compare x y)
          where
          aux : Tri (x < y) (x ≈ y) (x > y) → C
          aux (tri< _ _ _) = x
          aux (tri≈ _ _ _) = x
          aux (tri> _ _ _) = y

  lemma :  ∀ x y → x < y → min x y ≡ x
  lemma x y x<y =
                ?
-------------------------------------------------------------------


Thanks,

------
Sergei