[Agda] decidable equality in algebra

[Sergei Meshveliani]

People,

My DoCon-A library currently requires DecSetoid as a base for all the
computer algebra.
But I think about making _≟_ optional.
Because I think, for example, that a Real number can be reasonably
represented as a certain sequence of embedded seqments, so that it will
be possible to prove in Agda that Real has the instances of
CommutativeRing and Field. But equality will not be solvable there.

(only I mean a real Real, do not confuse with floating point).

However I expect that most known algorithms will require various
complicated additional witness arguments to be correct for the case of
real numbers.
For example, for univariate polynomials over Rational coefficients it is
easy to resolve the divisibility relation.
And for Real coefficients, resolving the relation

             (x + c) divides (x^2 + a*x + b)        (1)

is equivalent to resolving 
                             b - (a-c)*c ≈ 0        (2)

-- a witness for (1) is reduced to a witness for (2).
For arbitrary polynomials over Real, the corresponding condition will be
complicated.

Anyone here dealt with constructive methods for arbitrary real numbers? 
(the Coq users mentioned some library). 

I wonder of how many nice algorithms are known for real numbers, whether
they are interesting so that it could be worthy to lift the ≟
requirement. 

Thanks,

------
Sergei