# [Agda] trivial lemma of `with'

Sergei Meshveliani mechvel at botik.ru
Mon Dec 30 18:23:52 CET 2013

```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

```