[Agda] trivial lemma of `with'

[Sergei Meshveliani]

Please, how to prove the below lemma?

------------------------------------------------------------------
open import Level using (Level; _⊔_)
open import Relation.Nullary using (¬_; yes; no)
open import Relation.Binary using (IsEquivalence; module IsEquivalence;
                                                           Decidable)
open import Algebra    using (Semiring; module Semiring)
open import Data.Empty using (⊥-elim)
      
module _ {α α=} (R : Semiring α α=)
  where
  open Semiring R using (_≈_; 0#)
                  renaming (Carrier to C; isEquivalence to ≈equiv)
  open IsEquivalence ≈equiv using (refl)

  record Foo : Set (α ⊔ α=)
    where
    field  _≟_  : Decidable _≈_
           dRem : (x y : C) → (y≉0 : ¬ y ≈ 0#) → C

    eQuot : C → C → C
    eQuot x y  with y ≟ 0#
    ...      | yes _  = 0#
    ...      | no y≉0 = dRem x y y≉0

    lemma : {x y : C} → (y≉0 : ¬ y ≈ 0#) → eQuot x y ≈ dRem x y y≉0
    lemma {x} {y} y≉0 =  refl

{-  with y ≟ 0# 
    ...              | yes y=0 =  ⊥-elim (y≉0 y=0) 
    ...              | no _    =  refl                             
-}

The  development Agda of November ~20 2013 MAlonzo 
reports
eQuot  x y | y ≟ 0# != dRem x y y≉0 of type C
when checking that the expression refl has type
eQuot x y ≈ dRem x y y≉0


Thanks,

------
Sergei