[Agda] divmod-unique of Agda prelude

[Sergei Meshveliani]

People,

I try to accompany divmod-unique of Agda prelude with a certain
congruence: 

  DivMod-cong :  ∀ {a a' b b'} → a ≡ a' → b ≡ b' → (d  : DivMod a  b ) →
                                                   (d' : DivMod a' b') →
                                       quot d ≡ quot d' × rem d ≡ rem d'


1) Has Agda prelude something close to it?
2) I wonder: how to fix the below implementation?
   Agda reports that  eq  is not of the declared type
   (and I think that it is).

Regards,

------
Sergei


--------------------------------------------------------------------
open import Function using (_$_) 
open import Relation.Binary.PropositionalEquality as PE using 
                                                     (_≡_; _≢_)
open import Data.Product using (_×_)
open import Data.Nat using (ℕ; suc; _+_ ; _*_)                       
open PE.≡-Reasoning renaming (_≡⟨_⟩_ to _≡[_]_; begin_ to ≡begin_;
                                                _∎ to _≡end)
open import Prelude     using (NonZero) renaming (_<_ to _<'_)
open import Numeric.Nat.DivMod using (DivMod; quot; rem; rem-less;
                                      quot-rem-sound; divmod-unique)

open DivMod

DivMod-cong :  ∀ {a a' b b'} → a ≡ a' → b ≡ b' → (d  : DivMod a  b ) →
                                                 (d' : DivMod a' b') →
                                     quot d ≡ quot d' × rem d ≡ rem d'

DivMod-cong {a} {a'} {b} {b'} a≡a' b≡b' d d' =  eq
   where
   q'     = quot d';       r'         = rem d'
   r'<'b' = rem-less d';   q'b'+r'≡a' = quot-rem-sound d'

   r'<'b : r' <' b
   r'<'b = PE.subst (r' <'_) (PE.sym b≡b') r'<'b'

   q'b+r'≡a :  q' * b + r' ≡ a
   q'b+r'≡a =
            ≡begin q' * b + r'   ≡[ PE.cong (\x → q' * x + r') b≡b' ]
                   q' * b' + r'  ≡[ q'b'+r'≡a' ]
                   a'            ≡[ PE.sym a≡a' ]
                   a
            ≡end

   d'' : DivMod a b
   d'' = qr q' r' r'<'b q'b+r'≡a

   eq : quot d ≡ quot d'' × rem d ≡ rem d''
   eq = divmod-unique {a} {b} d d''
---------------------------------------------------------------------