[Agda] _<=_ and _<_

[Sergei Meshveliani]

Please, how to prove          x < y → x ≤ y

in the general setting under  lib-0.7  ?
Namely:

---------------------------------------------------------------------
<-then-≤ : (dto : DecTotalOrder _ _ _) →
           let open DecTotalOrder dto using (_≈_; _≤_) 
                                      renaming (Carrier to C)
           in
           (_<_ : Rel C _) → IsStrictTotalOrder _≈_ _<_ →
           {x y : C}       → x < y                      → x ≤ y

<-then-≤ dto _<_ isSTO {x} {y} x<y =   ??

{- how to implement?

  case  ≤total x y  of \ { (inj₁ x≤y) → x≤y
                         ; (inj₂ y≤x) →	?
       	       	       	 }
  case  compare x y  of \ { (tri≈ _   x=y _) → ≤refl x=y
                          ; (tri≈ x<y _   _) → ?
                          }
-}
  where
  open DecTotalOrder dto using (Carrier;_≈_; _≤_) renaming
                                                  (reflexive to ≤refl)
  open IsStrictTotalOrder isSTO using (compare)
  open Tri
-------------------------------------------------------------------------

2) Is the above signature an appropriate way to relate _≤_ to _<_ ?


Thank you in advance for explanation,

------
Sergei