[Agda] moving common from `with'

[Serge D. Mechveliani]

Please, what is the nicest way to move a common function from under
`with' ?

Consider the program 

  f : Nat -> Nat -> Nat
  f m n  with  m <=? n
  ...  | yes _ = g (suc m) where
                           g : Nat -> Nat 
                           g m = m + m + 1
  ...  | no _  = g (suc n) where
                           g : Nat -> Nat 
                           g m = m + m + 1

The neccessity of moving  g  out is stronger for the examples having 
larger expressions for  g.

I find that it works
  f m n = h    
          where
          g : Nat -> Nat     -- to be replaced
          g m = m + m + 1    -- with a larger code

          h : Nat
          h  with  m <= n
          ...  | yes _ = g (suc m)
          ...  | no _  = g (suc n)

But this looks a bit awkward, it introduces an additional function  h,
and its signature. This does not look as nice as the Haskell code

  f m n = (case compare m n of GT -> g (suc n)
                               _  -> g (suc m))
          where
          g :: Int -> Int   
          g m = m + m + 1

(apart of that the signature for  g  can be skipped in Haskell).

Thanks,
Sergei